P. 445 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44401-44500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rp-oelim2 44401	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 8611. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐵 ∧ 𝐵 ∈ 𝑉)) → Lim (𝐴 ↑o 𝐵))
Theorem	oeord2lim 44402	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 8598. (Contributed by RP, 30-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 1o ∈ 𝐴) ∧ (Lim 𝐶 ∧ 𝐶 ∈ 𝑉)) → (𝐵 ∈ 𝐶 → (𝐴 ↑o 𝐵) ∈ (𝐴 ↑o 𝐶)))
Theorem	oeord2i 44403	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 44404	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 44405	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 44406	Ordinal 3 is the unordered triple containing ordinals 0, 1, and 2. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, 1o, 2o}
Theorem	df3o3 44407	Ordinal 3, fully expanded. (Contributed by RP, 8-Jul-2021.)
⊢ 3o = {∅, {∅}, {∅, {∅}}}
Theorem	oenord1ex 44408	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 44409*	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 44410*	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 44411	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 44412*	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 44413	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 44414*	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 44415*	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 44416*	Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brslts 28150. (Contributed by RP, 26-Sep-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    ⇒   ⊢ (𝐴𝑅𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))
Theorem	cantnfresb 44417*	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 44418*	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.40.2  Natural addition of Cantor normal forms
Theorem	oawordex2 44419*	If 𝐶 is between 𝐴 (inclusive) and (𝐴 +o 𝐵) (exclusive), there is an ordinal which equals 𝐶 when summed to 𝐴. This is a slightly different statement than oawordex 8567 or oawordeu 8565. (Contributed by RP, 7-Jan-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 +o 𝐵))) → ∃𝑥 ∈ 𝐵 (𝐴 +o 𝑥) = 𝐶)
Theorem	nnawordexg 44420*	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 8648. (Contributed by RP, 7-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +o ω)) → ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)
Theorem	succlg 44421	Closure law for ordinal successor. (Contributed by RP, 8-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ (𝐵 = ∅ ∨ (𝐵 = (ω ·o 𝐶) ∧ 𝐶 ∈ (On ∖ 1o)))) → suc 𝐴 ∈ 𝐵)
Theorem	dflim5 44422*	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 44423	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 44424	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 44425	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 44426	Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 = ∅ ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	omcl3g 44427	Closure law for ordinal multiplication. (Contributed by RP, 14-Jan-2025.)
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ (𝐶 ∈ 3o ∨ (𝐶 = (ω ↑o (ω ↑o 𝐷)) ∧ 𝐷 ∈ On))) → (𝐴 ·o 𝐵) ∈ 𝐶)
Theorem	ordsssucb 44428	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 44495, limsssuc 7861. (Contributed by RP, 22-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
Theorem	tfsconcatlem 44429*	Lemma for tfsconcatun 44430. (Contributed by RP, 23-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ ((𝐴 +o 𝐵) ∖ 𝐴)) → ∃!𝑥∃𝑦 ∈ 𝐵 (𝐶 = (𝐴 +o 𝑦) ∧ 𝑥 = (𝐹‘𝑦)))
Theorem	tfsconcatun 44430*	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 44431*	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 44432*	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 44433*	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 44434*	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 44435*	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 44436*	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 44437*	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 44438*	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 44439*	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 44440*	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 44441*	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 44442*	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 44443*	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 44444*	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 44445	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 44446*	The limit of a sequence of ordinals is the union of its range. (Contributed by RP, 1-Mar-2025.)
⊢ (𝐴 Fn 𝐵 → ∪ 𝑥 ∈ 𝐵 (𝐴‘𝑥) = ∪ ran 𝐴)
Theorem	ofoafg 44447*	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 44448	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 44449	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 𝐴))
Theorem	ofoacl 44450	Closure law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ (𝐵 ∈ On ∧ 𝐶 = (ω ↑o 𝐵))) ∧ (𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐴))) → (𝐹 ∘f +o 𝐺) ∈ (𝐶 ↑m 𝐴))
Theorem	ofoaid1 44451	Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → (𝐹 ∘f +o (𝐴 × {∅})) = 𝐹)
Theorem	ofoaid2 44452	Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → ((𝐴 × {∅}) ∘f +o 𝐹) = 𝐹)
Theorem	ofoaass 44453	Component-wise addition of ordinal-yielding functions is associative. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ (𝐹 ∈ (𝐵 ↑m 𝐴) ∧ 𝐺 ∈ (𝐵 ↑m 𝐴) ∧ 𝐻 ∈ (𝐵 ↑m 𝐴))) → ((𝐹 ∘f +o 𝐺) ∘f +o 𝐻) = (𝐹 ∘f +o (𝐺 ∘f +o 𝐻)))
Theorem	ofoacom 44454	Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹 ∈ (ω ↑m 𝐴) ∧ 𝐺 ∈ (ω ↑m 𝐴))) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹))
Theorem	naddcnff 44455	Addition operator for Cantor normal forms is a function into Cantor normal forms. (Contributed by RP, 2-Jan-2025.)
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)):(𝑆 × 𝑆)⟶𝑆)
Theorem	naddcnffn 44456	Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.)
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆))
Theorem	naddcnffo 44457	Addition of Cantor normal forms is a function onto Cantor normal forms. (Contributed by RP, 2-Jan-2025.)
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)):(𝑆 × 𝑆)–onto→𝑆)
Theorem	naddcnfcl 44458	Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) ∈ 𝑆)
Theorem	naddcnfcom 44459	Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹))
Theorem	naddcnfid1 44460	Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → (𝐹 ∘f +o (𝑋 × {∅})) = 𝐹)
Theorem	naddcnfid2 44461	Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → ((𝑋 × {∅}) ∘f +o 𝐹) = 𝐹)
Theorem	naddcnfass 44462	Component-wise addition of Cantor normal forms is associative. (Contributed by RP, 3-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆)) → ((𝐹 ∘f +o 𝐺) ∘f +o 𝐻) = (𝐹 ∘f +o (𝐺 ∘f +o 𝐻)))
Theorem	onsucunifi 44463*	The successor to the union of any non-empty, finite subset of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.)
⊢ ((𝐴 ⊆ On ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → suc ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 suc 𝑥)
Theorem	sucunisn 44464	The successor to the union of any singleton of a set is the successor of the set. (Contributed by RP, 11-Feb-2025.)
⊢ (𝐴 ∈ 𝑉 → suc ∪ {𝐴} = suc 𝐴)
Theorem	onsucunipr 44465	The successor to the union of any pair of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc ∪ {𝐴, 𝐵} = ∪ {suc 𝐴, suc 𝐵})
Theorem	onsucunitp 44466	The successor to the union of any triple of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → suc ∪ {𝐴, 𝐵, 𝐶} = ∪ {suc 𝐴, suc 𝐵, suc 𝐶})
Theorem	oaun3lem1 44467*	The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 44475. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
Theorem	oaun3lem2 44468*	The class of all ordinal sums of elements from two ordinals is bounded by the sum. Lemma for oaun3 44475. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ (𝐴 +o 𝐵))
Theorem	oaun3lem3 44469*	The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 44475. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ On)
Theorem	oaun3lem4 44470*	The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 44475. (Contributed by RP, 12-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ suc (𝐴 +o 𝐵))
Theorem	rp-abid 44471*	Two ways to express a class. (Contributed by RP, 13-Feb-2025.)
⊢ 𝐴 = {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}
Theorem	oadif1lem 44472*	Express the set difference of a continuous sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊕ 𝐵) ∈ On)    &   ⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On) → (𝐴 ⊕ 𝑏) ∈ On)    &   ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ (𝐴 ⊕ 𝐵))) → ∃𝑏 ∈ 𝐵 (𝐴 ⊕ 𝑏) = 𝑦)    &   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝑏 ∈ 𝐵 → (𝐴 ⊕ 𝑏) ∈ (𝐴 ⊕ 𝐵)))    &   ⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On) → 𝐴 ⊆ (𝐴 ⊕ 𝑏))    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ⊕ 𝐵) ∖ 𝐴) = {𝑥 ∣ ∃𝑏 ∈ 𝐵 𝑥 = (𝐴 ⊕ 𝑏)})
Theorem	oadif1 44473*	Express the set difference of an ordinal sum and its left addend as a class of sums. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) ∖ 𝐴) = {𝑥 ∣ ∃𝑏 ∈ 𝐵 𝑥 = (𝐴 +o 𝑏)})
Theorem	oaun2 44474*	Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}})
Theorem	oaun3 44475*	Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}, {𝑧 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)}})
Theorem	naddov4 44476*	Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ ({𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 (𝑎 +no 𝐵) ∈ 𝑥} ∩ {𝑥 ∈ On ∣ ∀𝑏 ∈ 𝐵 (𝐴 +no 𝑏) ∈ 𝑥}))
Theorem	nadd2rabtr 44477*	The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Tr {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶})
Theorem	nadd2rabord 44478*	The set of ordinals which have a natural sum less than some ordinal is an ordinal. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Ord {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶})
Theorem	nadd2rabex 44479*	The class of ordinals which have a natural sum less than some ordinal is a set. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶} ∈ V)
Theorem	nadd2rabon 44480*	The set of ordinals which have a natural sum less than some ordinal is an ordinal number. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝐵 +no 𝑥) ∈ 𝐶} ∈ On)
Theorem	nadd1rabtr 44481*	The set of ordinals which have a natural sum less than some ordinal is transitive. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Tr {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶})
Theorem	nadd1rabord 44482*	The set of ordinals which have a natural sum less than some ordinal is an ordinal. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → Ord {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶})
Theorem	nadd1rabex 44483*	The class of ordinals which have a natural sum less than some ordinal is a set. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶} ∈ V)
Theorem	nadd1rabon 44484*	The set of ordinals which have a natural sum less than some ordinal is an ordinal number. (Contributed by RP, 20-Dec-2024.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → {𝑥 ∈ 𝐴 ∣ (𝑥 +no 𝐵) ∈ 𝐶} ∈ On)
Theorem	nadd1suc 44485	Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.)
⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴)
Theorem	naddass1 44486	Natural addition of ordinal numbers is associative when the third element is 1. (Contributed by RP, 1-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) +no 1o) = (𝐴 +no (𝐵 +no 1o)))
Theorem	naddgeoa 44487	Natural addition results in a value greater than or equal than that of ordinal addition. (Contributed by RP, 1-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ⊆ (𝐴 +no 𝐵))
Theorem	naddonnn 44488	Natural addition with a natural number on the right results in a value equal to that of ordinal addition. (Contributed by RP, 1-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (𝐴 +no 𝐵))
Theorem	naddwordnexlem0 44489	When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, (ω ·o suc 𝐶) lies between 𝐴 and 𝐵. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → (𝐴 ∈ (ω ·o suc 𝐶) ∧ (ω ·o suc 𝐶) ⊆ 𝐵))
Theorem	naddwordnexlem1 44490	When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, 𝐵 is equal to or larger than 𝐴. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	naddwordnexlem2 44491	When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, 𝐵 is larger than 𝐴. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐵)
Theorem	naddwordnexlem3 44492*	When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, every natural sum of 𝐴 with a natural number is less that 𝐵. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ ω (𝐴 +no 𝑥) ∈ 𝐵)
Theorem	oawordex3 44493*	When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, some ordinal sum of 𝐴 is equal to 𝐵. This is a specialization of oawordex 8567. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵)
Theorem	naddwordnexlem4 44494*	When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, there exists a product with omega such that the ordinal sum with 𝐴 is less than or equal to 𝐵 while the natural sum is larger than 𝐵. (Contributed by RP, 15-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    &   ⊢ 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥))))
Theorem	ordsssucim 44495	If an ordinal is less than or equal to the successor of another, then the first is either less than or equal to the second or the first is equal to the successor of the second. Theorem 1 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 See also ordsssucb 44428 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
Theorem	insucid 44496	The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∩ suc 𝐴) = 𝐴
Theorem	oaltom 44497	Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴)))
Theorem	oe2 44498	Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o))
Theorem	omltoe 44499	Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴)))
21.40.3  Surreal Contributions
Theorem	abeqabi 44500	Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.)
⊢ 𝐴 = {𝑥 ∣ 𝜓}    ⇒   ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓))