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	oneptri 44101	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 44102	Membership in the difference of ordinals. (Contributed by RP, 15-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐶 ∈ (𝐴 ∖ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ⊆ 𝐶)))
Theorem	ordeldifsucon 44103	Membership in the difference of ordinal and successor ordinal. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On) → (𝐶 ∈ (𝐴 ∖ suc 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)))
Theorem	ordeldif1o 44104	Membership in the difference of ordinal and ordinal one. (Contributed by RP, 16-Jan-2025.)
⊢ (Ord 𝐴 → (𝐵 ∈ (𝐴 ∖ 1o) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅)))
Theorem	ordne0gt0 44105	Ordinal zero is less than every nonzero ordinal. Theorem 1.10 of [Schloeder] p. 2. Closely related to ord0eln0 6414. (Contributed by RP, 16-Jan-2025.)
⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴)
Theorem	ondif1i 44106	Ordinal zero is less than every nonzero ordinal, class difference version. Theorem 1.10 of [Schloeder] p. 2. See ondif1 8491. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ (On ∖ 1o) → ∅ ∈ 𝐴)
Theorem	onsucelab 44107*	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 44108*	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 44109*	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 44110	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 7815. (Contributed by RP, 16-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴))
Theorem	ordnexbtwnsuc 44111*	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 44112	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 44113*	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 44114*	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 44115*	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 44116*	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 44117*	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 7845. (Contributed by RP, 17-Jan-2025.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∀𝑏 ∈ 𝐴 suc 𝑏 ∈ 𝐴 ∧ 𝐴 ≠ ∅))
Theorem	onov0suclim 44118	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 44119*	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 8506, oasuc 8514, and oalim 8522. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 +o 𝐵) = 𝐴) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 +o 𝐵) = suc (𝐴 +o 𝐶)) ∧ (Lim 𝐵 → (𝐴 +o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 +o 𝑐))))
Theorem	om0suclim 44120*	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 8507, omsuc 8516, and omlim 8523. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ·o 𝐵) = ∅) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ·o 𝐵) = ((𝐴 ·o 𝐶) +o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ·o 𝐵) = ∪ 𝑐 ∈ 𝐵 (𝐴 ·o 𝑐))))
Theorem	oe0suclim 44121*	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 8512, oesuc 8517, oe0m1 8511, and oelim 8524. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 = ∅ → (𝐴 ↑o 𝐵) = 1o) ∧ ((𝐵 = suc 𝐶 ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐵) = ((𝐴 ↑o 𝐶) ·o 𝐴)) ∧ (Lim 𝐵 → (𝐴 ↑o 𝐵) = if(∅ ∈ 𝐴, ∪ 𝑐 ∈ 𝐵 (𝐴 ↑o 𝑐), ∅))))
Theorem	oaomoecl 44122	The operations of addition, multiplication, and exponentiation are closed. Remark 2.8 of [Schloeder] p. 5. See oacl 8525, omcl 8526, oecl 8527. (Contributed by RP, 18-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ↑o 𝐵) ∈ On))
Theorem	onsupsucismax 44123*	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 44124*	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 44125	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 44126*	A limit ordinal is the union of its elements, indexed union version. Lemma 2.13 of [Schloeder] p. 5. See limuni 6420. (Contributed by RP, 27-Jan-2025.)
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥)
Theorem	limexissupab 44127*	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 44128	Ordinal one is both a left and right identity of ordinal multiplication. Lemma 2.15 of [Schloeder] p. 5. See om1 8532 and om1r 8533 for individual statements. (Contributed by RP, 29-Jan-2025.)
⊢ (𝐴 ∈ On → ((1o ·o 𝐴) = (𝐴 ·o 1o) ∧ (𝐴 ·o 1o) = 𝐴))
Theorem	oe0rif 44129	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 44130*	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 44131	Natural numbers are closed under ordinal addition, multiplication, and exponentiation. Theorem 2.20 of [Schloeder] p. 6. See nnacl 8602, nnmcl 8603, nnecl 8604. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 +o 𝐵) ∈ ω ∧ (𝐴 ·o 𝐵) ∈ ω ∧ (𝐴 ↑o 𝐵) ∈ ω))
Theorem	onsucwordi 44132	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 44133	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 44134	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 44135	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 44136	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 44137	Ordinal one plus omega is equal to omega. See oaabs 8639 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 8640 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 44138	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 44139	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 44140*	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 44141	Any nonzero ordinal product is greater-than-or-equal to the term on the left. Lemma 3.11 of [Schloeder] p. 8. See omword1 8563. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ·o 𝐵))
Theorem	omge2 44142	Any nonzero ordinal product is greater-than-or-equal to the term on the right. Lemma 3.12 of [Schloeder] p. 9. See omword2 8564. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ≠ ∅) → 𝐵 ⊆ (𝐴 ·o 𝐵))
Theorem	omlim2 44143	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 44144	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 44145	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 44146	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 44147	Ordinal two times omega is omega. Lemma 3.17 of [Schloeder] p. 10. (Contributed by RP, 30-Jan-2025.)
⊢ (2o ·o ω) = ω
Theorem	omnord1ex 44148	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 44149*	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 44150	Any nonzero ordinal power is greater-than-or-equal to the term on the left. Lemma 3.19 of [Schloeder] p. 10. See oewordi 8582. (Contributed by RP, 29-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐵 ≠ ∅) → 𝐴 ⊆ (𝐴 ↑o 𝐵))
Theorem	oege2 44151	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 8584. (Contributed by RP, 29-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ 𝐵 ∈ On) → 𝐵 ⊆ (𝐴 ↑o 𝐵))
Theorem	rp-oelim2 44152	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 8591. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ↑o 𝐵))
Theorem	oeord2lim 44153	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 8578. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	oeord2i 44154	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 44155	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 44156	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 44157	Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, 1o, 2o}
Theorem	df3o3 44158	Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, {∅}, {∅, {∅}}}
Theorem	oenord1ex 44159	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 44160*	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 44161*	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 44162	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 44163*	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 44164	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 44165*	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 44166*	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 44167*	Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brslts 28030. (Contributed by RP, 26-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))
Theorem	cantnfresb 44168*	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 44169*	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 44170*	If 𝐶 is between 𝐴 (inclusive) and (𝐴 +o 𝐵) (exclusive), there is an ordinal which equals 𝐶 when summed to 𝐴. This is a slightly different statement than oawordex 8547 or oawordeu 8545. (Contributed by RP, 7-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 +o 𝐵))) → ∃𝑥 ∈ 𝐵 (𝐴 +o 𝑥) = 𝐶)
Theorem	nnawordexg 44171*	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 8628. (Contributed by RP, 7-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +o ω)) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)
Theorem	succlg 44172	Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐵 = ∅ ∨ (𝐵 = (ω ·o 𝐶) ∧ 𝐶 ∈ (On ∖ 1o)))) → suc 𝐴 ∈ 𝐵)
Theorem	dflim5 44173*	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 44174	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 44175	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 44176	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 44177	Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	omcl3g 44178	Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	ordsssucb 44179	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 44246, limsssuc 7847. (Contributed by RP, 22-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
Theorem	tfsconcatlem 44180*	Lemma for tfsconcatun 44181. (Contributed by RP, 23-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ((𝐴 +o 𝐵) ∖ 𝐴)) → ∃!𝑥∃𝑦 ∈ 𝐵 (𝐶 = (𝐴 +o 𝑦) ∧ 𝑥 = (𝐹‘𝑦)))
Theorem	tfsconcatun 44181*	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 44182*	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 44183*	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 44184*	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 44185*	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 44186*	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 44187*	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 44188*	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 44189*	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 44190*	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 44191*	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 44192*	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 44193*	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 44194*	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 44195*	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)))
Theorem	tfsnfin 44196	A transfinite sequence is infinite iff its domain is greater than or equal to omega. Theorem 5 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, 1-Mar-2025.)
⊢ ((𝐴 Fn 𝐵 ∧ 𝐵 ∈ On) → (¬ 𝐴 ∈ Fin ↔ ω ⊆ 𝐵))
Theorem	rp-tfslim 44197*	The limit of a sequence of ordinals is the union of its range. (Contributed by RP, 1-Mar-2025.)
⊢ (𝐴 Fn 𝐵 → ∪ 𝑥 ∈ 𝐵 (𝐴‘𝑥) = ∪ ran 𝐴)
Theorem	ofoafg 44198*	Addition operator for functions from sets into ordinals results in a function from the intersection of sets into an ordinal. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 ∈ On ∧ 𝐹 = ∪ 𝑑 ∈ 𝐷 (𝑑 +o 𝐸))) → ( ∘f +o ↾ ((𝐷 ↑m 𝐴) × (𝐸 ↑m 𝐵))):((𝐷 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐹 ↑m 𝐶))
Theorem	ofoaf 44199	Addition operator for functions from sets into power of omega results in a function from the intersection of sets to that power of omega. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷))) → ( ∘f +o ↾ ((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))):((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐸 ↑m 𝐶))
Theorem	ofoafo 44200	Addition operator for functions from a set into a power of omega is an onto binary operator. (Contributed by RP, 5-Jan-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) → ( ∘f +o ↾ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐴))):((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐴))–onto→(𝐶 ↑m 𝐴))