Theory ordinalBasic

⊢ allOrds = mkWO {(x,y) | x = y ∨ x < y}

⊢ ∀s. cardSUC s = preds (csuc (oleast a. preds a ≈ s))

⊢ ∀a. csuc a = oleast b. preds a ≺ preds b

⊢ ∀s. dclose s = {x | ∃y. y ∈ s ∧ x < y}

⊢ ∀s. downward_closed s ⇔ ∀a b. a ∈ s ∧ b < a ⇒ b ∈ s

⊢ 0 = (oleast a. T) ∧ ∀n. &SUC n = (&n)⁺

⊢ ∀P. $oleast P = @x. P x ∧ ∀y. y < x ⇒ ¬P y

⊢ ∀s. omax s = some a. maximal_elements s {(x,y) | x ≤ y} = {a}

⊢ ω = sup {(&i) | T}

⊢ ∀b. b + 0 = b ∧ (∀a. b + a⁺ = (b + a)⁺) ∧
      ∀a. 0 < a ∧ islimit a ⇒ b + a = sup (IMAGE ($+ b) (preds a))

⊢ ∀a. a⁺ = oleast b. a < b

⊢ ∀r. mkOrdinal r = ordinal_ABS_CLASS (orderiso r)

⊢ ∀a. ordinal_REP a = $@ (ordinal_REP_CLASS a)

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. orderiso r r ∧ c = orderiso r) rep

⊢ (∀a. ordinal_ABS_CLASS (ordinal_REP_CLASS a) = a) ∧
  ∀r. (λc. ∃r. orderiso r r ∧ c = orderiso r) r ⇔
      ordinal_REP_CLASS (ordinal_ABS_CLASS r) = r

⊢ ∀T1 T2. T1 < T2 ⇔ orderlt (ordinal_REP T1) (ordinal_REP T2)

⊢ ∀w. preds w = {w0 | w0 < w}

⊢ ∀ordset. sup ordset = oleast a. a ∉ BIGUNION (IMAGE preds ordset)

⊢ FINITE (cardSUC A) ⇔ FINITE A

⊢ s ≠ ∅ ∧ FINITE s ⇒ ∃a. omax s = SOME a

⊢ FINITE (preds a) ⇔ ∃n. a = &n

⊢ (x ≠ 0 ⇔ 0 < x) ∧ (1 ≤ x ⇔ 0 < x)

⊢ ω ≤ x ⇒ INFINITE {y | preds y ≈ preds x}

⊢ x ∈ preds w ⇔ x < w

⊢ 0⁺ = 1

⊢ 𝕌(:num) ≼ 𝕌(:num + α)

⊢ (x,y) WIN allOrds ⇔ x < y

⊢ 0o < csuc a ∧ csuc a ≠ 0o

⊢ 𝕌(:num + α) ≺ 𝕌(:num + (α + num -> bool))

⊢ cardSUC A ≠ ∅

⊢ s ≼ 𝕌(:num + α) ⇒ ∃a. preds a ≈ s

⊢ ∀x. ∃y. preds x ≺ preds y

⊢ ω ≤ x ⇒ {y | preds y ≼ preds x} ≈ {y | preds y ≈ preds x}

⊢ preds a ≼ preds b ⇒ preds (csuc a) ≼ preds (csuc b)

⊢ ω ≤ x ⇒ preds x ≺ {y | preds y ≈ preds x}

⊢ preds x ≺ {y | preds y ≼ preds x}

⊢ preds x ≺ preds y ⇒ x < y

⊢ csuc a = &n ⇔ ∃m. n = SUC m ∧ a = &m

⊢ ω ≤ a ⇒ islimit (csuc a) ∧ 0o < csuc a

⊢ countable s ⇒ ∀d. d ∈ s ⇒ d ≤ sup s

⊢ countable s ⇒ (sup s ≤ b ⇔ ∀d. d ∈ s ⇒ d ≤ b)

⊢ countable s ⇒ ∀b. b < sup s ⇔ ∃d. d ∈ s ∧ b < d

⊢ dclose s = BIGUNION (IMAGE preds s)

⊢ elsOf allOrds = 𝕌(:α ordinal)

⊢ ∀x y. &x = &y ⇔ x = y

⊢ ∀n. &SUC n = (&n)⁺

⊢ 0 = (oleast a. T) ∧
  (∀n. & <..num comp'n..> = (&(<..num comp'n..> − 1))⁺) ∧
  ∀n. & <..num comp'n..> = (& <..num comp'n..> )⁺

⊢ ∀n. &n ≠ ω

⊢ ∀n. &n < ω

⊢ &n < &m ⇔ n < m

⊢ islimit x⁺ ⇔ F

⊢ islimit b ∧ a < b ⇒ a⁺ < b

⊢ islimit (&x) ⇔ x = 0

⊢ A ≼ cardSUC A

⊢ ∀x a. x ≤ a + x

⊢ A ≺ cardSUC A

⊢ x < csuc y ⇔ preds x ≼ preds y

⊢ ∀a. a < ω ⇔ ∃m. a = &m

⊢ ∀b. b < sup (preds a) ⇔ ∃d. d < a ∧ b < d

⊢ ∀a. mkOrdinal (ordinal_REP a) = a

⊢ ∀a. ∃b. a < b

⊢ ∀Q P. (∃a. P a) ∧ (∀a. (∀b. b < a ⇒ ¬P b) ∧ P a ⇒ Q a) ⇒ Q ($oleast P)

⊢ omax ∅ = NONE

⊢ omax (x INSERT y) = if ∀e. e ∈ y ⇒ e ≤ x then SOME x else omax y

⊢ omax s = NONE ⇔ ∀a. a ∈ s ⇒ ∃b. b ∈ s ∧ a < b

⊢ omax s = SOME a ⇔ a ∈ s ∧ ∀b. b ∈ s ⇒ b ≤ a

⊢ omax (preds a⁺) = SOME a

⊢ islimit ω

⊢ INFINITE (preds a) ⇒ ω ≤ a

⊢ islimit ω

⊢ ∀a. 0 + a = a

⊢ (∀c a. a = a + c ⇔ c = 0) ∧ ∀c a. a + c = a ⇔ c = 0

⊢ ∀b a c. a < b ⇒ c + a < c + b

⊢ ∀b a c. a + b = a + c ⇔ b = c

⊢ &n + &m = &(n + m)

⊢ &n + ω = ω

⊢ a⁺ = b⁺ ⇔ a = b

⊢ a⁺ < b⁺ ⇔ a < b

⊢ (& <..num comp'n..> )⁺ = &(<..num comp'n..> + 1)

⊢ a⁺ ≠ 0

⊢ 0 < x⁺

⊢ ∀a. a = 0 ∨ (∃a0. a = a0⁺) ∨ 0 < a ∧ islimit a

⊢ ∀z sf lf. ∃h.
    h 0 = z ∧ (∀a. h a⁺ = sf a (h a)) ∧
    ∀a. 0 < a ∧ islimit a ⇒ h a = lf a (IMAGE h (preds a))

⊢ (∀min. (∀b. b < min ⇒ P b) ⇒ P min) ⇒ ∀a. P a

⊢ orderiso w1 w2 ⇒ elsOf w1 ≈ elsOf w2

⊢ ∀r s. orderiso r s ⇔ mkOrdinal r = mkOrdinal s

⊢ orderiso (wobound x w) (wobound y w) ⇒ (x,y) ∉ strict (destWO w)

⊢ orderiso w1 w2 ⇒ ¬orderlt w1 w2

⊢ (∀a. ordinal_ABS_CLASS (ordinal_REP_CLASS a) = a) ∧
  ∀c. (∃r. orderiso r r ∧ c = orderiso r) ⇔
      ordinal_REP_CLASS (ordinal_ABS_CLASS c) = c

⊢ QUOTIENT orderiso mkOrdinal ordinal_REP

⊢ a ≤ b ∧ b ≤ a ⇒ a = b

⊢ ∀a b. a ≤ b ⇔ ∃c. b = a + c

⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z

⊢ a ≤ b ⇔ a < b ∨ a = b

⊢ x ≤ 0 ⇔ x = 0

⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z

⊢ ∀b a c. c + a < c + b ⇔ a < b

⊢ a + b < a ⇔ F

⊢ ∀b a. a < a + b ⇔ 0 < b

⊢ ¬(a < b ∧ b < a⁺)

⊢ ∀a b. a < b ⇔ ∃c. c ≠ 0 ∧ b = a + c

⊢ ∀w. w ≤ w

⊢ a < a⁺

⊢ a < b⁺ ⇔ a < b ∨ a = b

⊢ ∀w1 w2 w3. w1 < w2 ∧ w2 < w3 ⇒ w1 < w3

⊢ WF $<

⊢ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. b < min ⇒ ¬B b

⊢ 0 ≤ a

⊢ ∀n x. x < &n ⇔ ∃m. x = &m ∧ m < n

⊢ o1 < o2 ⇔ ∀w1 w2. mkOrdinal w1 = o1 ∧ mkOrdinal w2 = o2 ⇒ orderlt w1 w2

⊢ ∀w2 w1. w1 < w2 ∨ w1 = w2 ∨ w2 < w1

⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z

⊢ ∀b. b < sup (IMAGE f (preds a)) ⇔ ∃d. d < a ∧ b < f d

⊢ preds 0 = ∅

⊢ preds w1 = preds w2 ⇔ w1 = w2

⊢ preds x = ∅ ⇔ x = 0

⊢ BIJ preds 𝕌(:α ordinal) (downward_closed DELETE 𝕌(:α ordinal))

⊢ preds a ≼ preds (csuc a)

⊢ downward_closed (preds w)

⊢ preds ord ≼ 𝕌(:num + α)

⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ ∀d. d ∈ s ⇒ d ≤ sup s

⊢ w1 < w2 ⇔ preds w1 ⊂ preds w2

⊢ preds (&n) = IMAGE $& (count n)

⊢ omax (preds a) = SOME b ⇔ a = b⁺

⊢ preds a⁺ = a INSERT preds a

⊢ s ≼ 𝕌(:num + α) ⇒ preds (sup s) = dclose s

⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ ∀b. b < sup s ⇔ ∃d. d ∈ s ∧ b < d

⊢ downward_closed s ∧ s ≠ 𝕌(:α ordinal) ⇒ (sup s ≤ b ⇔ ∀d. d ∈ s ⇒ d ≤ b)

⊢ ∀x. downward_closed x ∧ x ≠ 𝕌(:α ordinal) ⇒ ∃y. preds y = x

⊢ preds ord = elsOf (wobound ord allOrds)

⊢ ∀P. P 0 ∧ (∀a. P a ⇒ P a⁺) ∧
      (∀a. islimit a ∧ 0 < a ∧ (∀b. b < a ⇒ P b) ⇒ P a) ⇒
      ∀a. P a

⊢ sup ∅ = 0

⊢ s ≼ 𝕌(:num + α) ⇒ (sup s = 0 ⇔ s = ∅ ∨ s = {0})

⊢ sup {a} = a

⊢ (∀b. b ∈ s ⇒ b ≤ a) ∧ a ∈ s ⇒ sup s = a

⊢ sup (preds a⁺) = a

⊢ islimit a ⇔ sup (preds a) = a

⊢ s ≼ 𝕌(:num + α) ⇒ ∀a. a < sup s ⇔ ∃b. b ∈ s ∧ a < b

⊢ ∀b s. s ≼ 𝕌(:num + α) ∧ b ∈ s ⇒ b ≤ sup s

⊢ ∀a. preds a ≼ 𝕌(:num + β) ⇒
      ∃b. orderiso (wobound a allOrds) (wobound b allOrds) ∧
          preds a ≈ preds b

⊢ (∀a. a ∈ s ⇒ a < b) ⇒ ∀c. c < sup s ⇔ ∃d. d ∈ s ∧ c < d

⊢ 𝕌(:num + α) ≺ 𝕌(:α ordinal)

⊢ wellorder {(x,y) | x = y ∨ x < y}

⊢ ∀w. orderiso w (wobound (mkOrdinal w) allOrds)