P. 434 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43301-43400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tfsconcatfv1 43301*	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 43302*	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 43303*	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 43304*	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 43305*	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 43306*	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 43307*	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 43308*	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 43309*	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 43310*	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 43311*	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 43312*	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 43313*	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 43314	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 43315*	The limit of a sequence of ordinals is the union of its range. (Contributed by RP, 1-Mar-2025.)
⊢ (𝐴 Fn 𝐵 → ∪ 𝑥 ∈ 𝐵 (𝐴‘𝑥) = ∪ ran 𝐴)
Theorem	ofoafg 43316*	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 43317	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 43318	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 43319	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 43320	Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → (𝐹 ∘f +o (𝐴 × {∅})) = 𝐹)
Theorem	ofoaid2 43321	Identity law for component wise addition of ordinal-yielding functions. (Contributed by RP, 5-Jan-2025.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ On) ∧ 𝐹 ∈ (𝐵 ↑m 𝐴)) → ((𝐴 × {∅}) ∘f +o 𝐹) = 𝐹)
Theorem	ofoaass 43322	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 43323	Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.)
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐹 ∈ (ω ↑m 𝐴) ∧ 𝐺 ∈ (ω ↑m 𝐴))) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹))
Theorem	naddcnff 43324	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 43325	Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.)
⊢ ((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) → ( ∘f +o ↾ (𝑆 × 𝑆)) Fn (𝑆 × 𝑆))
Theorem	naddcnffo 43326	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 43327	Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) ∈ 𝑆)
Theorem	naddcnfcom 43328	Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ (𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆)) → (𝐹 ∘f +o 𝐺) = (𝐺 ∘f +o 𝐹))
Theorem	naddcnfid1 43329	Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → (𝐹 ∘f +o (𝑋 × {∅})) = 𝐹)
Theorem	naddcnfid2 43330	Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.)
⊢ (((𝑋 ∈ On ∧ 𝑆 = dom (ω CNF 𝑋)) ∧ 𝐹 ∈ 𝑆) → ((𝑋 × {∅}) ∘f +o 𝐹) = 𝐹)
Theorem	naddcnfass 43331	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 43332*	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 43333	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 43334	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 43335	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 43336*	The class of all ordinal sums of elements from two ordinals is ordinal. Lemma for oaun3 43344. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → Ord {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)})
Theorem	oaun3lem2 43337*	The class of all ordinal sums of elements from two ordinals is bounded by the sum. Lemma for oaun3 43344. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ⊆ (𝐴 +o 𝐵))
Theorem	oaun3lem3 43338*	The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 43344. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ On)
Theorem	oaun3lem4 43339*	The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 43344. (Contributed by RP, 12-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → {𝑥 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑥 = (𝑎 +o 𝑏)} ∈ suc (𝐴 +o 𝐵))
Theorem	rp-abid 43340*	Two ways to express a class. (Contributed by RP, 13-Feb-2025.)
⊢ 𝐴 = {𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}
Theorem	oadif1lem 43341*	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 43342*	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 43343*	Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}})
Theorem	oaun3 43344*	Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = ∪ {{𝑥 ∣ ∃𝑎 ∈ 𝐴 𝑥 = 𝑎}, {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = (𝐴 +o 𝑏)}, {𝑧 ∣ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 +o 𝑏)}})
Theorem	naddov4 43345*	Alternate expression for natural addition. (Contributed by RP, 19-Dec-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ ({𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 (𝑎 +no 𝐵) ∈ 𝑥} ∩ {𝑥 ∈ On ∣ ∀𝑏 ∈ 𝐵 (𝐴 +no 𝑏) ∈ 𝑥}))
Theorem	nadd2rabtr 43346*	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 43347*	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 43348*	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 43349*	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 43350*	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 43351*	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 43352*	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 43353*	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 43354	Natural addition with 1 is same as successor. (Contributed by RP, 31-Dec-2024.)
⊢ (𝐴 ∈ On → (𝐴 +no 1o) = suc 𝐴)
Theorem	naddass1 43355	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 43356	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 43357	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 43358	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 43359	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 43360	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 43361*	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 43362*	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 8613. (Contributed by RP, 14-Feb-2025.)
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀))    &   ⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁))    &   ⊢ (𝜑 → 𝐶 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ On)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝑁 ∈ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ On (𝐴 +o 𝑥) = 𝐵)
Theorem	naddwordnexlem4 43363*	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 43364	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 43297 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
Theorem	insucid 43365	The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∩ suc 𝐴) = 𝐴
Theorem	om2 43366	Two ways to double an ordinal. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐴 +o 𝐴) = (𝐴 ·o 2o))
Theorem	oaltom 43367	Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 +o 𝐴) ∈ (𝐵 ·o 𝐴)))
Theorem	oe2 43368	Two ways to square an ordinal. (Contributed by RP, 3-Jan-2025.)
⊢ (𝐴 ∈ On → (𝐴 ·o 𝐴) = (𝐴 ↑o 2o))
Theorem	omltoe 43369	Exponentiation eventually dominates multiplication. (Contributed by RP, 3-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((1o ∈ 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐵 ·o 𝐴) ∈ (𝐵 ↑o 𝐴)))
21.36.3  Surreal Contributions
Theorem	abeqabi 43370	Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.)
⊢ 𝐴 = {𝑥 ∣ 𝜓}    ⇒   ⊢ ({𝑥 ∣ 𝜑} = 𝐴 ↔ ∀𝑥(𝜑 ↔ 𝜓))
Theorem	abpr 43371*	Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑌 ∨ 𝑥 = 𝑍)))
Theorem	abtp 43372*	Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} = {𝑋, 𝑌, 𝑍} ↔ ∀𝑥(𝜑 ↔ (𝑥 = 𝑋 ∨ 𝑥 = 𝑌 ∨ 𝑥 = 𝑍)))
Theorem	ralopabb 43373*	Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.)
⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}    &   ⊢ (𝑜 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∀𝑜 ∈ 𝑂 𝜓 ↔ ∀𝑥∀𝑦(𝜑 → 𝜒))
Theorem	fpwfvss 43374	Functions into a powerset always have values which are subsets. This is dependant on our convention when the argument is not part of the domain. (Contributed by RP, 13-Sep-2024.)
⊢ 𝐹:𝐶⟶𝒫 𝐵    ⇒   ⊢ (𝐹‘𝐴) ⊆ 𝐵
Theorem	sdomne0 43375	A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.)
⊢ (𝐵 ≺ 𝐴 → 𝐴 ≠ ∅)
Theorem	sdomne0d 43376	A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.)
⊢ (𝜑 → 𝐵 ≺ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	safesnsupfiss 43377	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ⊆ 𝐵)
Theorem	safesnsupfiub 43378*	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑥𝑅𝑦)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)∀𝑦 ∈ 𝐶 𝑥𝑅𝑦)
Theorem	safesnsupfidom1o 43379	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o)
Theorem	safesnsupfilb 43380*	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 3-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦)
Theorem	isoeq145d 43381	Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)))
Theorem	resisoeq45d 43382	Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷)))
Theorem	negslem1 43383	An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.)
⊢ (𝐴 = 𝐵 → ((𝐹 ↾ 𝐴) Isom 𝑅, ◡𝑅(𝐴, 𝐴) ↔ (𝐹 ↾ 𝐵) Isom 𝑅, ◡𝑅(𝐵, 𝐵)))
Theorem	nvocnvb 43384*	Equivalence to saying the converse of an involution is the function itself. (Contributed by RP, 13-Oct-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) ↔ (𝐹:𝐴–1-1-onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥))
Theorem	rp-brsslt 43385*	Binary relation form of a relation, <, which has been extended from relation 𝑅 to subsets of class 𝑆. Usually, we will assume 𝑅 Or 𝑆. Definition in [Alling], p. 2. Generalization of brsslt 27848. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    ⇒   ⊢ (𝐴 < 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥𝑅𝑦)))
Theorem	nla0002 43386*	Extending a linear order to subsets, the empty set is less than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ∅ < 𝐴)
Theorem	nla0003 43387*	Extending a linear order to subsets, the empty set is greater than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝐴 < ∅)
Theorem	nla0001 43388*	Extending a linear order to subsets, the empty set is less than itself. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    ⇒   ⊢ (𝜑 → ∅ < ∅)
Theorem	faosnf0.11b 43389*	𝐵 is called a non-limit ordinal if it is not a limit ordinal. (Contributed by RP, 27-Sep-2023.) Alling, Norman L. "Fundamentals of Analysis Over Surreal Numbers Fields." The Rocky Mountain Journal of Mathematics 19, no. 3 (1989): 565-73. http://www.jstor.org/stable/44237243.
⊢ ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	dfno2 43390	A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025.)
⊢ No = {𝑓 ∈ 𝒫 (On × {1o, 2o}) ∣ (Fun 𝑓 ∧ dom 𝑓 ∈ On)}
Theorem	onnog 43391	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → (𝐴 × {𝐵}) ∈ No )
Theorem	onnobdayg 43392	Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → ( bday ‘(𝐴 × {𝐵})) = 𝐴)
Theorem	bdaybndex 43393	Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → (𝐵 × {𝐶}) ∈ No )
Theorem	bdaybndbday 43394	Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.)
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → ( bday ‘(𝐵 × {𝐶})) = ( bday ‘𝐴))
Theorem	onno 43395	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (𝐴 ∈ On → (𝐴 × {2o}) ∈ No )
Theorem	onnoi 43396	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 × {2o}) ∈ No
Theorem	0no 43397	Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ ∅ ∈ No
Theorem	1no 43398	Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (1o × {2o}) ∈ No
Theorem	2no 43399	Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (2o × {2o}) ∈ No
Theorem	3no 43400	Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (3o × {2o}) ∈ No