P. 433 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43201-43300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	onexgt 43201*	For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ 𝑥)
Theorem	onexomgt 43202*	For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ·o 𝑥))
Theorem	omlimcl2 43203	The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐵 ·o 𝐴))
Theorem	onexlimgt 43204*	For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On (Lim 𝑥 ∧ 𝐴 ∈ 𝑥))
Theorem	onexoegt 43205*	For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑥 ∈ On 𝐴 ∈ (ω ↑o 𝑥))
Theorem	oninfex2 43206*	The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∪ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦} ∈ V)
Theorem	onsupeqmax 43207*	Condition when the supremum of a set of ordinals is the maximum element of that set. (Contributed by RP, 24-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥 ↔ ∪ 𝐴 ∈ 𝐴))
Theorem	onsupeqnmax 43208*	Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025.)
⊢ (𝐴 ⊆ On → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ (∪ 𝐴 = ∪ ∪ 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴)))
Theorem	onsuplub 43209*	The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ 𝐵 ∈ On) → (𝐵 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝐵 ∈ 𝑧))
Theorem	onsupnub 43210*	An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.)
⊢ (((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ On ∧ ∀𝑧 ∈ 𝐴 𝑧 ⊆ 𝐵)) → ∪ 𝐴 ⊆ 𝐵)
Theorem	onfisupcl 43211	Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9354. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∪ 𝐴 ∈ 𝐴))
Theorem	onelord 43212	Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6420 and eloni 6405. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	onepsuc 43213	Every ordinal is less than its successor, relationship version. Lemma 1.7 of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ (𝐴 ∈ On → 𝐴 E suc 𝐴)
Theorem	epsoon 43214	The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7810 and weso 5691. (Contributed by RP, 15-Jan-2025.)
⊢ E Or On
Theorem	epirron 43215	The strict order on the ordinals is irreflexive. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ (𝐴 ∈ On → ¬ 𝐴 E 𝐴)
Theorem	oneptr 43216	The strict order on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 E 𝐵 ∧ 𝐵 E 𝐶) → 𝐴 E 𝐶))
Theorem	oneltr 43217	The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6441. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	oneptri 43218	The strict, complete (linear) order on the ordinals is complete. Theorem 1.9(iii) of [Schloeder] p. 1. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 E 𝐵 ∨ 𝐵 E 𝐴 ∨ 𝐴 = 𝐵))
Theorem	oneltri 43219	The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of [Schloeder] p. 1. See ordtri3or 6427. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ∨ 𝐴 = 𝐵))
Theorem	ordeldif 43220	Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	ordeldifsucon 43221	Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)))
Theorem	ordeldif1o 43222	Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.)
⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅)))
Theorem	ordne0gt0 43223	Ordinal zero is less than every non-zero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6450. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
Theorem	ondif1i 43224	Ordinal zero is less than every non-zero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8557. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴)
Theorem	onsucelab 43225*	The successor of every ordinal is an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏})
Theorem	dflim6 43226*	A limit ordinal is a non-zero ordinal which is not a successor ordinal. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃𝑏 ∈ On 𝐴 = suc 𝑏))
Theorem	limnsuc 43227*	A limit ordinal is not an element of the class of successor ordinals. Definition 1.11 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ (Lim 𝐴 → ¬ 𝐴 ∈ {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏})
Theorem	onsucss 43228	If one ordinal is less than another, then the successor of the first is less than or equal to the second. Lemma 1.13 of [Schloeder] p. 2. See ordsucss 7854. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴))
Theorem	ordnexbtwnsuc 43229*	For any distinct pair of ordinals, if there is no ordinal between the lesser and the greater, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 16-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ord 𝐵) → (∀𝑐 ∈ On ¬ (𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵) → 𝐵 = suc 𝐴))
Theorem	orddif0suc 43230	For any distinct pair of ordinals, if the set difference between the greater and the successor of the lesser is empty, the greater is the successor of the lesser. Lemma 1.16 of [Schloeder] p. 2. (Contributed by RP, 17-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ord 𝐵) → ((𝐵 ∖ suc 𝐴) = ∅ → 𝐵 = suc 𝐴))
Theorem	onsucf1lem 43231*	For ordinals, the successor operation is injective, so there is at most one ordinal that a given ordinal could be the successor of. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ (𝐴 ∈ On → ∃*𝑏 ∈ On 𝐴 = suc 𝑏)
Theorem	onsucf1olem 43232*	The successor operation is bijective between the ordinals and the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴) → ∃!𝑏 ∈ On 𝐴 = suc 𝑏)
Theorem	onsucrn 43233*	The successor operation is surjective onto its range, the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ 𝐹 = (𝑥 ∈ On ↦ suc 𝑥)    ⇒   ⊢ ran 𝐹 = {𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏}
Theorem	onsucf1o 43234*	The successor operation is a bijective function between the ordinals and the class of successor ordinals. Lemma 1.17 of [Schloeder] p. 2. (Contributed by RP, 18-Jan-2025.)
⊢ 𝐹 = (𝑥 ∈ On ↦ suc 𝑥)    ⇒   ⊢ 𝐹:On–1-1-onto→{𝑎 ∈ On ∣ ∃𝑏 ∈ On 𝑎 = suc 𝑏}
Theorem	dflim7 43235*	A limit ordinal is a non-zero ordinal that contains all the successors of its elements. Lemma 1.18 of [Schloeder] p. 2. Closely related to dflim4 7885. (Contributed by RP, 17-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∀𝑏 ∈ 𝐴 suc 𝑏 ∈ 𝐴 ∧ 𝐴 ≠ ∅))
Theorem	onov0suclim 43236	Compactly express rules for binary operations on ordinals. (Contributed by RP, 18-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐴 ⊗ ∅) = 𝐷)    &   ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊗ suc 𝐶) = 𝐸)    &   ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝐵) → (𝐴 ⊗ 𝐵) = 𝐹)    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ⊗ 𝐵) = 𝐷) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ⊗ 𝐵) = 𝐸) ∧ (Lim 𝐵 → (𝐴 ⊗ 𝐵) = 𝐹)))
Theorem	oa0suclim 43237*	Closed form expression of the value of ordinal addition for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.3 of [Schloeder] p. 4. See oa0 8572, oasuc 8580, and oalim 8588. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 +o 𝐵) = 𝐴) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 +o 𝐵) = suc (𝐴 +o 𝐶)) ∧ (Lim 𝐵 → (𝐴 +o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 +o 𝑐))))
Theorem	om0suclim 43238*	Closed form expression of the value of ordinal multiplication for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.5 of [Schloeder] p. 4. See om0 8573, omsuc 8582, and omlim 8589. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = ((𝐴 ·o 𝐶) +o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ·o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 ·o 𝑐))))
Theorem	oe0suclim 43239*	Closed form expression of the value of ordinal exponentiation for the cases when the second ordinal is zero, a successor ordinal, or a limit ordinal. Definition 2.6 of [Schloeder] p. 4. See oe0 8578, oesuc 8583, oe0m1 8577, and oelim 8590. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ↑o 𝐵) = 1o) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐵) = ((𝐴 ↑o 𝐶) ·o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅))))
Theorem	oaomoecl 43240	The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8591, omcl 8592, oecl 8593. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ↑o 𝐵) ∈ On))
Theorem	onsupsucismax 43241*	If the union of a set of ordinals is a successor ordinal, then that union is the maximum element of the set. This is not a bijection because sets where the maximum element is zero or a limit ordinal exist. Lemma 2.11 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → (∃𝑏 ∈ On ∪ 𝐴 = suc 𝑏 → ∪ 𝐴 ∈ 𝐴))
Theorem	onsssupeqcond 43242*	If for every element of a set of ordinals there is an element of a subset which is at least as large, then the union of the set and the subset is the same. Lemma 2.12 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ 𝑉) → ((𝐵 ⊆ 𝐴 ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 ⊆ 𝑏) → ∪ 𝐴 = ∪ 𝐵))
Theorem	limexissup 43243	An ordinal which is a limit ordinal is equal to its supremum. Lemma 2.13 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 = sup(𝐴, On, E ))
Theorem	limiun 43244*	A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6456. (Contributed by RP, 27-Jan-2025.)
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥)
Theorem	limexissupab 43245*	An ordinal which is a limit ordinal is equal to the supremum of the class of all its elements. Lemma 2.13 of [Schloeder] p. 5. (Contributed by RP, 27-Jan-2025.)
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 = sup({𝑥 ∣ 𝑥 ∈ 𝐴}, On, E ))
Theorem	om1om1r 43246	Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8598 and om1r 8599 for individual statements. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ∈ On → ((1o ·o 𝐴) = (𝐴 ·o 1o) ∧ (𝐴 ·o 1o) = 𝐴))
Theorem	oe0rif 43247	Ordinal zero raised to any non-zero ordinal power is zero and zero to the zeroth power is one. Lemma 2.18 of [Schloeder] p. 6. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ∈ On → (∅ ↑o 𝐴) = if(∅ ∈ 𝐴, ∅, 1o))
Theorem	oasubex 43248*	While subtraction can't be a binary operation on ordinals, for any pair of ordinals there exists an ordinal that can be added to the lessor (or equal) one which will sum to the greater. Theorem 2.19 of [Schloeder] p. 6. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ⊆ 𝐴) → ∃𝑐 ∈ On (𝑐 ⊆ 𝐴 ∧ (𝐵 +o 𝑐) = 𝐴))
Theorem	nnamecl 43249	Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8667, nnmcl 8668, nnecl 8669. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 +o 𝐵) ∈ ω ∧ (𝐴 ·o 𝐵) ∈ ω ∧ (𝐴 ↑o 𝐵) ∈ ω))
Theorem	onsucwordi 43250	The successor operation preserves the less-than-or-equal relationship between ordinals. Lemma 3.1 of [Schloeder] p. 7. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → suc 𝐴 ⊆ suc 𝐵))
Theorem	oalim2cl 43251	The ordinal sum of any ordinal with a limit ordinal on the right is a limit ordinal. (Contributed by RP, 6-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ Lim 𝐵 ∧ 𝐵 ∈ 𝑉) → Lim (𝐴 +o 𝐵))
Theorem	oaltublim 43252	Given 𝐶 is a limit ordinal, the sum of any ordinal with an ordinal less than 𝐶 is less than the sum of the first ordinal with 𝐶. Lemma 3.5 of [Schloeder] p. 7. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐶 ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐴 +o 𝐵) ∈ (𝐴 +o 𝐶))
Theorem	oaordi3 43253	Ordinal addition of the same number on the left preserves the ordering of the numbers on the right. Lemma 3.6 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 +o 𝐵) ∈ (𝐴 +o 𝐶)))
Theorem	oaord3 43254	When the same ordinal is added on the left, ordering of the sums is equivalent to the ordering of the ordinals on the right. Theorem 3.7 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 ↔ (𝐴 +o 𝐵) ∈ (𝐴 +o 𝐶)))
Theorem	1oaomeqom 43255	Ordinal one plus omega is equal to omega. See oaabs 8704 for the sum of any natural number on the left and ordinal at least as large as omega on the right. Lemma 3.8 of [Schloeder] p. 8. See oaabs2 8705 where a power of omega is the upper bound of the left and a lower bound on the right. (Contributed by RP, 29-Jan-2025.)
⊢ (1o +o ω) = ω
Theorem	oaabsb 43256	The right addend absorbs the sum with an ordinal iff that ordinal times omega is less than or equal to the right addend. (Contributed by RP, 19-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o ω) ⊆ 𝐵 ↔ (𝐴 +o 𝐵) = 𝐵))
Theorem	oaordnrex 43257	When omega is added on the right to ordinals zero and one, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ¬ (∅ ∈ 1o ↔ (∅ +o ω) ∈ (1o +o ω))
Theorem	oaordnr 43258*	When the same ordinal is added on the right, ordering of the sums is not equivalent to the ordering of the ordinals on the left. Remark 3.9 of [Schloeder] p. 8. (Contributed by RP, 29-Jan-2025.)
⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ∃𝑐 ∈ On ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 +o 𝑐) ∈ (𝑏 +o 𝑐))
Theorem	omge1 43259	Any non-zero ordinal product is greater-than-or-equal to the term on the left. Lemma 3.11 of [Schloeder] p. 8. See omword1 8629. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ·o 𝐵))
Theorem	omge2 43260	Any non-zero ordinal product is greater-than-or-equal to the term on the right. Lemma 3.12 of [Schloeder] p. 9. See omword2 8630. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ⊆ (𝐴 ·o 𝐵))
Theorem	omlim2 43261	The non-zero product with an limit ordinal on the right is a limit ordinal. Lemma 3.13 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ·o 𝐵))
Theorem	omord2lim 43262	Given a limit ordinal, the product of any non-zero ordinal with an ordinal less than that limit ordinal is less than the product of the non-zero ordinal with the limit ordinal . Lemma 3.14 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))
Theorem	omord2i 43263	Ordinal multiplication of the same non-zero number on the left preserves the ordering of the numbers on the right. Lemma 3.15 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))
Theorem	omord2com 43264	When the same non-zero ordinal is multiplied on the left, ordering of the products is equivalent to the ordering of the ordinals on the right. Theorem 3.16 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴) ↔ (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))
Theorem	2omomeqom 43265	Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.)
⊢ (2o ·o ω) = ω
Theorem	omnord1ex 43266	When omega is multiplied on the right to ordinals one and two, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of [Schloeder] p. 10. (Contributed by RP, 29-Jan-2025.)
⊢ ¬ (1o ∈ 2o ↔ (1o ·o ω) ∈ (2o ·o ω))
Theorem	omnord1 43267*	When the same non-zero ordinal is multiplied on the right, ordering of the products is not equivalent to the ordering of the ordinals on the left. Remark 3.18 of [Schloeder] p. 10. (Contributed by RP, 4-Feb-2025.)
⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐))
Theorem	oege1 43268	Any non-zero ordinal power is greater-than-or-equal to the term on the left. Lemma 3.19 of [Schloeder] p. 10. See oewordi 8647. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ↑o 𝐵))
Theorem	oege2 43269	Any power of an ordinal at least as large as two is greater-than-or-equal to the term on the right. Lemma 3.20 of [Schloeder] p. 10. See oeworde 8649. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐵 ∈ On) → 𝐵 ⊆ (𝐴 ↑o 𝐵))
Theorem	rp-oelim2 43270	The power of an ordinal at least as large as two with a limit ordinal on thr right is a limit ordinal. Lemma 3.21 of [Schloeder] p. 10. See oelimcl 8656. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ↑o 𝐵))
Theorem	oeord2lim 43271	Given a limit ordinal, the power of any base at least as large as two raised to an ordinal less than that limit ordinal is less than the power of that base raised to the limit ordinal . Lemma 3.22 of [Schloeder] p. 10. See oeordi 8643. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	oeord2i 43272	Ordinal exponentiation of the same base at least as large as two preserves the ordering of the exponents. Lemma 3.23 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	oeord2com 43273	When the same base at least as large as two is raised to ordinal powers, , ordering of the power is equivalent to the ordering of the exponents. Theorem 3.24 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 ↔ (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	nnoeomeqom 43274	Any natural number at least as large as two raised to the power of omega is omega. Lemma 3.25 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
⊢ ((𝐴 ∈ ω ∧ 1o ∈ 𝐴) → (𝐴 ↑o ω) = ω)
Theorem	df3o2 43275	Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, 1o, 2o}
Theorem	df3o3 43276	Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, {∅}, {∅, {∅}}}
Theorem	oenord1ex 43277	When ordinals two and three are both raised to the power of omega, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
⊢ ¬ (2o ∈ 3o ↔ (2o ↑o ω) ∈ (3o ↑o ω))
Theorem	oenord1 43278*	When two ordinals (both at least as large as two) are raised to the same power, ordering of the powers is not equivalent to the ordering of the bases. Remark 3.26 of [Schloeder] p. 11. (Contributed by RP, 4-Feb-2025.)
⊢ ∃𝑎 ∈ (On ∖ 2o)∃𝑏 ∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))
Theorem	oaomoencom 43279*	Ordinal addition, multiplication, and exponentiation do not generally commute. Theorem 4.1 of [Schloeder] p. 11. (Contributed by RP, 30-Jan-2025.)
⊢ (∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 +o 𝑏) = (𝑏 +o 𝑎) ∧ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ·o 𝑏) = (𝑏 ·o 𝑎) ∧ ∃𝑎 ∈ On ∃𝑏 ∈ On ¬ (𝑎 ↑o 𝑏) = (𝑏 ↑o 𝑎))
Theorem	oenassex 43280	Ordinal two raised to two to the zeroth power is not the same as two squared then raised to the zeroth power. (Contributed by RP, 30-Jan-2025.)
⊢ ¬ (2o ↑o (2o ↑o ∅)) = ((2o ↑o 2o) ↑o ∅)
Theorem	oenass 43281*	Ordinal exponentiation is not associative. Remark 4.6 of [Schloeder] p. 14. (Contributed by RP, 30-Jan-2025.)
⊢ ∃𝑎 ∈ On ∃𝑏 ∈ On ∃𝑐 ∈ On ¬ (𝑎 ↑o (𝑏 ↑o 𝑐)) = ((𝑎 ↑o 𝑏) ↑o 𝑐)
Theorem	cantnftermord 43282	For terms of the form of a power of omega times a non-zero natural number, ordering of the exponents implies ordering of the terms. Lemma 5.1 of [Schloeder] p. 15. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ (ω ∖ 1o) ∧ 𝐷 ∈ (ω ∖ 1o))) → (𝐴 ∈ 𝐵 → ((ω ↑o 𝐴) ·o 𝐶) ∈ ((ω ↑o 𝐵) ·o 𝐷)))
Theorem	cantnfub 43283*	Given a finite number of terms of the form ((ω ↑o (𝐴‘𝑛)) ·o (𝑀‘𝑛)) with distinct exponents, we may order them from largest to smallest and find the sum is less than (ω ↑o 𝑋) when (𝐴‘𝑛) is less than 𝑋 and (𝑀‘𝑛) is less than ω. Lemma 5.2 of [Schloeder] p. 15. (Contributed by RP, 31-Jan-2025.)
⊢ (𝜑 → 𝑋 ∈ On)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝐴:𝑁–1-1→𝑋)    &   ⊢ (𝜑 → 𝑀:𝑁⟶ω)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅))    ⇒   ⊢ (𝜑 → (𝐹 ∈ dom (ω CNF 𝑋) ∧ ((ω CNF 𝑋)‘𝐹) ∈ (ω ↑o 𝑋)))
Theorem	cantnfub2 43284*	Given a finite number of terms of the form ((ω ↑o (𝐴‘𝑛)) ·o (𝑀‘𝑛)) with distinct exponents, we may order them from largest to smallest and find the sum is less than (ω ↑o suc ∪ ran 𝐴) when (𝑀‘𝑛) is less than ω. Lemma 5.2 of [Schloeder] p. 15. (Contributed by RP, 9-Feb-2025.)
⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝐴:𝑁–1-1→On)    &   ⊢ (𝜑 → 𝑀:𝑁⟶ω)    &   ⊢ 𝐹 = (𝑥 ∈ suc ∪ ran 𝐴 ↦ if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅))    ⇒   ⊢ (𝜑 → (suc ∪ ran 𝐴 ∈ On ∧ 𝐹 ∈ dom (ω CNF suc ∪ ran 𝐴) ∧ ((ω CNF suc ∪ ran 𝐴)‘𝐹) ∈ (ω ↑o suc ∪ ran 𝐴)))
Theorem	bropabg 43285*	Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27848. (Contributed by RP, 26-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))
Theorem	cantnfresb 43286*	A Cantor normal form which sums to less than a certain power has only zeros for larger components. (Contributed by RP, 3-Feb-2025.)
⊢ (((𝐴 ∈ (On ∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))
Theorem	cantnf2 43287*	For every ordinal, 𝐴, there is a an ordinal exponent 𝑏 such that 𝐴 is less than (ω ↑o 𝑏) and for every ordinal at least as large as 𝑏 there is a unique Cantor normal form, 𝑓, with zeros for all the unnecessary higher terms, that sums to 𝐴. Theorem 5.3 of [Schloeder] p. 16. (Contributed by RP, 3-Feb-2025.)
⊢ (𝐴 ∈ On → ∃𝑏 ∈ On ∀𝑐 ∈ (On ∖ 𝑏)∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴)))
21.36.2  Natural addition of Cantor normal forms
Theorem	oawordex2 43288*	If 𝐶 is between 𝐴 (inclusive) and (𝐴 +o 𝐵) (exclusive), there is an ordinal which equals 𝐶 when summed to 𝐴. This is a slightly different statement than oawordex 8613 or oawordeu 8611. (Contributed by RP, 7-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 +o 𝐵))) → ∃𝑥 ∈ 𝐵 (𝐴 +o 𝑥) = 𝐶)
Theorem	nnawordexg 43289*	If an ordinal, 𝐵, is in a half-open interval between some 𝐴 and the next limit ordinal, 𝐵 is the sum of the 𝐴 and some natural number. This weakens the antecedent of nnawordex 8693. (Contributed by RP, 7-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +o ω)) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)
Theorem	succlg 43290	Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐵 = ∅ ∨ (𝐵 = (ω ·o 𝐶) ∧ 𝐶 ∈ (On ∖ 1o)))) → suc 𝐴 ∈ 𝐵)
Theorem	dflim5 43291*	A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025.)
⊢ (Lim 𝐴 ↔ (𝐴 = On ∨ ∃𝑥 ∈ (On ∖ 1o)𝐴 = (ω ·o 𝑥)))
Theorem	oacl2g 43292	Closure law for ordinal addition. Here we show that ordinal addition is closed within the empty set or any ordinal power of omega. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o 𝐷) ∧ 𝐷 ∈ On))) → (𝐴 +o 𝐵) ∈ 𝐶)
Theorem	onmcl 43293	If an ordinal is less than a power of omega, the product with a natural number is also less than that power of omega. (Contributed by RP, 19-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑁 ∈ ω) → (𝐴 ∈ (ω ↑o 𝐵) → (𝐴 ·o 𝑁) ∈ (ω ↑o 𝐵)))
Theorem	omabs2 43294	Ordinal multiplication by a larger ordinal is absorbed when the larger ordinal is either 2 or ω raised to some power of ω. (Contributed by RP, 12-Jan-2025.)
⊢ (((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐴) ∧ (𝐵 = ∅ ∨ 𝐵 = 2o ∨ (𝐵 = (ω ↑o (ω ↑o 𝐶)) ∧ 𝐶 ∈ On))) → (𝐴 ·o 𝐵) = 𝐵)
Theorem	omcl2 43295	Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	omcl3g 43296	Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	ordsssucb 43297	An ordinal number is less than or equal to the successor of an ordinal class iff the ordinal number is either less than or equal to the ordinal class or the ordinal number is equal to the successor of the ordinal class. See also ordsssucim 43364, limsssuc 7887. (Contributed by RP, 22-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
Theorem	tfsconcatlem 43298*	Lemma for tfsconcatun 43299. (Contributed by RP, 23-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ((𝐴 +o 𝐵) ∖ 𝐴)) → ∃!𝑥∃𝑦 ∈ 𝐵 (𝐶 = (𝐴 +o 𝑦) ∧ 𝑥 = (𝐹‘𝑦)))
Theorem	tfsconcatun 43299*	The concatenation of two transfinite series is a union of functions. (Contributed by RP, 23-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 + 𝐵) = (𝐴 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐶 +o 𝐷) ∖ 𝐶) ∧ ∃𝑧 ∈ 𝐷 (𝑥 = (𝐶 +o 𝑧) ∧ 𝑦 = (𝐵‘𝑧)))}))
Theorem	tfsconcatfn 43300*	The concatenation of two transfinite series is a transfinite series. (Contributed by RP, 22-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 + 𝐵) Fn (𝐶 +o 𝐷))