P. 442 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44101-44200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	onepsuc 44101	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 44102	The ordinals are strictly and completely (linearly) ordered. Theorem 1.9 of [Schloeder] p. 1. Based on epweon 7778 and weso 5650. (Contributed by RP, 15-Jan-2025.)
⊢ E Or On
Theorem	epirron 44103	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 44104	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 44105	The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of [Schloeder] p. 1. See ontr1 6409. (Contributed by RP, 15-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	oneptri 44106	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	ordeldif 44107	Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	ordeldifsucon 44108	Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)))
Theorem	ordeldif1o 44109	Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.)
⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅)))
Theorem	ordne0gt0 44110	Ordinal zero is less than every nonzero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6418. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
Theorem	ondif1i 44111	Ordinal zero is less than every nonzero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8492. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴)
Theorem	onsucelab 44112*	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 44113*	A limit ordinal is a nonzero 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 44114*	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 44115	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 7818. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴))
Theorem	ordnexbtwnsuc 44116*	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 44117	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 44118*	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 44119*	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 44120*	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 44121*	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 44122*	A limit ordinal is a nonzero ordinal that contains all the successors of its elements. Lemma 1.18 of [Schloeder] p. 2. Closely related to dflim4 7848. (Contributed by RP, 17-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∀𝑏 ∈ 𝐴 suc 𝑏 ∈ 𝐴 ∧ 𝐴 ≠ ∅))
Theorem	onov0suclim 44123	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 44124*	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 8507, oasuc 8515, and oalim 8523. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 +o 𝐵) = 𝐴) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 +o 𝐵) = suc (𝐴 +o 𝐶)) ∧ (Lim 𝐵 → (𝐴 +o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 +o 𝑐))))
Theorem	om0suclim 44125*	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 8508, omsuc 8517, and omlim 8524. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = ((𝐴 ·o 𝐶) +o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ·o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 ·o 𝑐))))
Theorem	oe0suclim 44126*	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 8513, oesuc 8518, oe0m1 8512, and oelim 8525. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ↑o 𝐵) = 1o) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐵) = ((𝐴 ↑o 𝐶) ·o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅))))
Theorem	oaomoecl 44127	The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8526, omcl 8527, oecl 8528. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ↑o 𝐵) ∈ On))
Theorem	onsupsucismax 44128*	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 44129*	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 44130	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 44131*	A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6424. (Contributed by RP, 27-Jan-2025.)
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥)
Theorem	limexissupab 44132*	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 44133	Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8533 and om1r 8534 for individual statements. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ∈ On → ((1o ·o 𝐴) = (𝐴 ·o 1o) ∧ (𝐴 ·o 1o) = 𝐴))
Theorem	oe0rif 44134	Ordinal zero raised to any nonzero 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 44135*	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 44136	Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8603, nnmcl 8604, nnecl 8605. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 +o 𝐵) ∈ ω ∧ (𝐴 ·o 𝐵) ∈ ω ∧ (𝐴 ↑o 𝐵) ∈ ω))
Theorem	onsucwordi 44137	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 44138	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 44139	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 44140	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 44141	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 44142	Ordinal one plus omega is equal to omega. See oaabs 8640 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 8641 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 44143	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 44144	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 44145*	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 44146	Any nonzero ordinal product is greater-than-or-equal to the term on the left. Lemma 3.11 of [Schloeder] p. 8. See omword1 8564. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ·o 𝐵))
Theorem	omge2 44147	Any nonzero ordinal product is greater-than-or-equal to the term on the right. Lemma 3.12 of [Schloeder] p. 9. See omword2 8565. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ⊆ (𝐴 ·o 𝐵))
Theorem	omlim2 44148	The nonzero 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 44149	Given a limit ordinal, the product of any nonzero ordinal with an ordinal less than that limit ordinal is less than the product of the nonzero ordinal with the limit ordinal . Lemma 3.14 of [Schloeder] p. 9. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐴 ≠ ∅) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ·o 𝐵) ∈ (𝐴 ·o 𝐶)))
Theorem	omord2i 44150	Ordinal multiplication of the same nonzero 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 44151	When the same nonzero 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 44152	Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.)
⊢ (2o ·o ω) = ω
Theorem	omnord1ex 44153	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 44154*	When the same nonzero 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 44155	Any nonzero ordinal power is greater-than-or-equal to the term on the left. Lemma 3.19 of [Schloeder] p. 10. See oewordi 8583. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ↑o 𝐵))
Theorem	oege2 44156	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 8585. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐵 ∈ On) → 𝐵 ⊆ (𝐴 ↑o 𝐵))
Theorem	rp-oelim2 44157	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 8592. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ↑o 𝐵))
Theorem	oeord2lim 44158	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 8579. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	oeord2i 44159	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 44160	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 44161	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 44162	Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, 1o, 2o}
Theorem	df3o3 44163	Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, {∅}, {∅, {∅}}}
Theorem	oenord1ex 44164	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 44165*	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 44166*	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 44167	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 44168*	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 44169	For terms of the form of a power of omega times a nonzero 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 44170*	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 44171*	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 44172*	Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brslts 28035. (Contributed by RP, 26-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))
Theorem	cantnfresb 44173*	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 44174*	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.38.2  Natural addition of Cantor normal forms
Theorem	oawordex2 44175*	If 𝐶 is between 𝐴 (inclusive) and (𝐴 +o 𝐵) (exclusive), there is an ordinal which equals 𝐶 when summed to 𝐴. This is a slightly different statement than oawordex 8548 or oawordeu 8546. (Contributed by RP, 7-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 +o 𝐵))) → ∃𝑥 ∈ 𝐵 (𝐴 +o 𝑥) = 𝐶)
Theorem	nnawordexg 44176*	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 8629. (Contributed by RP, 7-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +o ω)) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)
Theorem	succlg 44177	Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐵 = ∅ ∨ (𝐵 = (ω ·o 𝐶) ∧ 𝐶 ∈ (On ∖ 1o)))) → suc 𝐴 ∈ 𝐵)
Theorem	dflim5 44178*	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 44179	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 44180	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 44181	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 44182	Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	omcl3g 44183	Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	ordsssucb 44184	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 44251, limsssuc 7850. (Contributed by RP, 22-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
Theorem	tfsconcatlem 44185*	Lemma for tfsconcatun 44186. (Contributed by RP, 23-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ((𝐴 +o 𝐵) ∖ 𝐴)) → ∃!𝑥∃𝑦 ∈ 𝐵 (𝐶 = (𝐴 +o 𝑦) ∧ 𝑥 = (𝐹‘𝑦)))
Theorem	tfsconcatun 44186*	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 44187*	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 𝐷))
Theorem	tfsconcatfv1 44188*	An early value of the concatenation of two transfinite series. (Contributed by RP, 23-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑋 ∈ 𝐶) → ((𝐴 + 𝐵)‘𝑋) = (𝐴‘𝑋))
Theorem	tfsconcatfv2 44189*	A latter value of the concatenation of two transfinite series. (Contributed by RP, 23-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑋 ∈ 𝐷) → ((𝐴 + 𝐵)‘(𝐶 +o 𝑋)) = (𝐵‘𝑋))
Theorem	tfsconcatfv 44190*	The value of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ ((((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) ∧ 𝑋 ∈ (𝐶 +o 𝐷)) → ((𝐴 + 𝐵)‘𝑋) = if(𝑋 ∈ 𝐶, (𝐴‘𝑋), (𝐵‘(℩𝑑 ∈ 𝐷 (𝐶 +o 𝑑) = 𝑋))))
Theorem	tfsconcatrn 44191*	The range of the concatenation of two transfinite series. (Contributed by RP, 24-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ran (𝐴 + 𝐵) = (ran 𝐴 ∪ ran 𝐵))
Theorem	tfsconcatfo 44192*	The concatenation of two transfinite series is onto the union of the ranges. (Contributed by RP, 24-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 + 𝐵):(𝐶 +o 𝐷)–onto→(ran 𝐴 ∪ ran 𝐵))
Theorem	tfsconcatb0 44193*	The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 25-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐵 = ∅ ↔ (𝐴 + 𝐵) = 𝐴))
Theorem	tfsconcat0i 44194*	The concatentation with the empty series leaves the series unchanged. (Contributed by RP, 28-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (𝐴 = ∅ → (𝐴 + 𝐵) = 𝐵))
Theorem	tfsconcat0b 44195*	The concatentation with the empty series leaves the finite series unchanged. (Contributed by RP, 1-Mar-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ ω)) → (𝐴 = ∅ ↔ (𝐴 + 𝐵) = 𝐵))
Theorem	tfsconcat00 44196*	The concatentation of two empty series results in an empty series. (Contributed by RP, 25-Feb-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 + 𝐵) = ∅))
Theorem	tfsconcatrev 44197*	If the domain of a transfinite sequence is an ordinal sum, the sequence can be decomposed into two sequences with domains corresponding to the addends. Theorem 2 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ ((𝐹 Fn (𝐶 +o 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ∃𝑢 ∈ (ran 𝐹 ↑m 𝐶)∃𝑣 ∈ (ran 𝐹 ↑m 𝐷)((𝑢 + 𝑣) = 𝐹 ∧ dom 𝑢 = 𝐶 ∧ dom 𝑣 = 𝐷))
Theorem	tfsconcatrnss12 44198*	The range of the concatenation of transfinite sequences is a superset of the ranges of both sequences. Theorem 3 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (ran 𝐴 ⊆ ran (𝐴 + 𝐵) ∧ ran 𝐵 ⊆ ran (𝐴 + 𝐵)))
Theorem	tfsconcatrnss 44199*	The concatenation of transfinite sequences yields elements from a class iff both sequences yield elements from that class. (Contributed by RP, 2-Mar-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (ran (𝐴 + 𝐵) ⊆ 𝑋 ↔ (ran 𝐴 ⊆ 𝑋 ∧ ran 𝐵 ⊆ 𝑋)))
Theorem	tfsconcatrnsson 44200*	The concatenation of transfinite sequences yields ordinals iff both sequences yield ordinals. Theorem 4 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 (Contributed by RP, 2-Mar-2025.)
⊢ + = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑎 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((dom 𝑎 +o dom 𝑏) ∖ dom 𝑎) ∧ ∃𝑧 ∈ dom 𝑏(𝑥 = (dom 𝑎 +o 𝑧) ∧ 𝑦 = (𝑏‘𝑧)))}))    ⇒   ⊢ (((𝐴 Fn 𝐶 ∧ 𝐵 Fn 𝐷) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → (ran (𝐴 + 𝐵) ⊆ On ↔ (ran 𝐴 ⊆ On ∧ ran 𝐵 ⊆ On)))