P. 88 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	4onn 8701	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
⊢ 4o ∈ ω
Theorem	1one2o 8702	Ordinal one is not ordinal two. Analogous to 1ne2 12501. (Contributed by AV, 17-Oct-2023.)
⊢ 1o ≠ 2o
Theorem	oaabslem 8703	Lemma for oaabs 8704. (Contributed by NM, 9-Dec-2004.)
⊢ ((ω ∈ On ∧ 𝐴 ∈ ω) → (𝐴 +o ω) = ω)
Theorem	oaabs 8704	Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of [TakeutiZaring] p. 59. (Contributed by NM, 9-Dec-2004.) (Proof shortened by Mario Carneiro, 29-May-2015.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ On) ∧ ω ⊆ 𝐵) → (𝐴 +o 𝐵) = 𝐵)
Theorem	oaabs2 8705	The absorption law oaabs 8704 is also a property of higher powers of ω. (Contributed by Mario Carneiro, 29-May-2015.)
⊢ (((𝐴 ∈ (ω ↑o 𝐶) ∧ 𝐵 ∈ On) ∧ (ω ↑o 𝐶) ⊆ 𝐵) → (𝐴 +o 𝐵) = 𝐵)
Theorem	omabslem 8706	Lemma for omabs 8707. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ ((ω ∈ On ∧ 𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → (𝐴 ·o ω) = ω)
Theorem	omabs 8707	Ordinal multiplication is also absorbed by powers of ω. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ (((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) ∧ (𝐵 ∈ On ∧ ∅ ∈ 𝐵)) → (𝐴 ·o (ω ↑o 𝐵)) = (ω ↑o 𝐵))
Theorem	nnm1 8708	Multiply an element of ω by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (𝐴 ·o 1o) = 𝐴)
Theorem	nnm2 8709	Multiply an element of ω by 2o. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (𝐴 ·o 2o) = (𝐴 +o 𝐴))
Theorem	nn2m 8710	Multiply an element of ω by 2o. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ω → (2o ·o 𝐴) = (𝐴 +o 𝐴))
Theorem	nnneo 8711	If a natural number is even, its successor is odd. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = (2o ·o 𝐴)) → ¬ suc 𝐶 = (2o ·o 𝐵))
Theorem	nneob 8712*	A natural number is even iff its successor is odd. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ (𝐴 ∈ ω → (∃𝑥 ∈ ω 𝐴 = (2o ·o 𝑥) ↔ ¬ ∃𝑥 ∈ ω suc 𝐴 = (2o ·o 𝑥)))
Theorem	omsmolem 8713*	Lemma for omsmo 8714. (Contributed by NM, 30-Nov-2003.) (Revised by David Abernethy, 1-Jan-2014.)
⊢ (𝑦 ∈ ω → (((𝐴 ⊆ On ∧ 𝐹:ω⟶𝐴) ∧ ∀𝑥 ∈ ω (𝐹‘𝑥) ∈ (𝐹‘suc 𝑥)) → (𝑧 ∈ 𝑦 → (𝐹‘𝑧) ∈ (𝐹‘𝑦))))
Theorem	omsmo 8714*	A strictly monotonic ordinal function on the set of natural numbers is one-to-one. (Contributed by NM, 30-Nov-2003.) (Revised by David Abernethy, 1-Jan-2014.)
⊢ (((𝐴 ⊆ On ∧ 𝐹:ω⟶𝐴) ∧ ∀𝑥 ∈ ω (𝐹‘𝑥) ∈ (𝐹‘suc 𝑥)) → 𝐹:ω–1-1→𝐴)
Theorem	omopthlem1 8715	Lemma for omopthi 8717. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐶 ∈ ω    ⇒   ⊢ (𝐴 ∈ 𝐶 → ((𝐴 ·o 𝐴) +o (𝐴 ·o 2o)) ∈ (𝐶 ·o 𝐶))
Theorem	omopthlem2 8716	Lemma for omopthi 8717. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐶 ∈ ω    &   ⊢ 𝐷 ∈ ω    ⇒   ⊢ ((𝐴 +o 𝐵) ∈ 𝐶 → ¬ ((𝐶 ·o 𝐶) +o 𝐷) = (((𝐴 +o 𝐵) ·o (𝐴 +o 𝐵)) +o 𝐵))
Theorem	omopthi 8717	An ordered pair theorem for ω. Theorem 17.3 of [Quine] p. 124. This proof is adapted from nn0opthi 14319. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 ∈ ω    &   ⊢ 𝐶 ∈ ω    &   ⊢ 𝐷 ∈ ω    ⇒   ⊢ ((((𝐴 +o 𝐵) ·o (𝐴 +o 𝐵)) +o 𝐵) = (((𝐶 +o 𝐷) ·o (𝐶 +o 𝐷)) +o 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))
Theorem	omopth 8718	An ordered pair theorem for finite integers. Analogous to nn0opthi 14319. (Contributed by Scott Fenton, 1-May-2012.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ ω)) → ((((𝐴 +o 𝐵) ·o (𝐴 +o 𝐵)) +o 𝐵) = (((𝐶 +o 𝐷) ·o (𝐶 +o 𝐷)) +o 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	nnasmo 8719*	There is at most one left additive inverse for natural number addition. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝐴 ∈ ω → ∃*𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)
Theorem	eldifsucnn 8720*	Condition for membership in the difference of ω and a nonzero finite ordinal. (Contributed by Scott Fenton, 24-Oct-2024.)
⊢ (𝐴 ∈ ω → (𝐵 ∈ (ω ∖ suc 𝐴) ↔ ∃𝑥 ∈ (ω ∖ 𝐴)𝐵 = suc 𝑥))
2.4.25  Natural addition
Syntax	cnadd 8721	Declare the syntax for natural ordinal addition. See df-nadd 8722.
class +no
Definition	df-nadd 8722*	Define natural ordinal addition. This is a commutative form of addition over the ordinals. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ +no = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1st ‘𝑧)} × (2nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st ‘𝑧) × {(2nd ‘𝑧)})) ⊆ 𝑤)}))
Theorem	on2recsfn 8723*	Show that double recursion over ordinals yields a function over pairs of ordinals. (Contributed by Scott Fenton, 3-Sep-2024.)
⊢ 𝐹 = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺)    ⇒   ⊢ 𝐹 Fn (On × On)
Theorem	on2recsov 8724*	Calculate the value of the double ordinal recursion operator. (Contributed by Scott Fenton, 3-Sep-2024.)
⊢ 𝐹 = frecs({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺)    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐹𝐵) = (⟨𝐴, 𝐵⟩𝐺(𝐹 ↾ ((suc 𝐴 × suc 𝐵) ∖ {⟨𝐴, 𝐵⟩}))))
Theorem	on2ind 8725*	Double induction over ordinal numbers. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ (𝑎 = 𝑐 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑐 → (𝜃 ↔ 𝜒))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑌 → (𝜏 ↔ 𝜂))    &   ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 𝜒 ∧ ∀𝑐 ∈ 𝑎 𝜓 ∧ ∀𝑑 ∈ 𝑏 𝜃) → 𝜑))    ⇒   ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On) → 𝜂)
Theorem	on3ind 8726*	Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024.)
⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))    &   ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))    &   ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))    &   ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))    &   ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))    &   ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))    &   ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))    &   ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (((∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁) ∧ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎) ∧ ∀𝑓 ∈ 𝑐 𝜂) → 𝜑))    ⇒   ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On) → 𝜆)
Theorem	coflton 8727*	Cofinality theorem for ordinals. If 𝐴 is cofinal with 𝐵 and 𝐵 precedes 𝐶, then 𝐴 precedes 𝐶. Compare cofsslt 27970 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝜑 → 𝐴 ⊆ On)    &   ⊢ (𝜑 → 𝐵 ⊆ On)    &   ⊢ (𝜑 → 𝐶 ⊆ On)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝑧 ∈ 𝑤)    ⇒   ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 𝑎 ∈ 𝑐)
Theorem	cofon1 8728*	Cofinality theorem for ordinals. If 𝐴 is cofinal with 𝐵 and the upper bound of 𝐴 dominates 𝐵, then their upper bounds are equal. Compare with cofcut1 27972 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 On)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)    &   ⊢ (𝜑 → 𝐵 ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧})    ⇒   ⊢ (𝜑 → ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} = ∩ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤})
Theorem	cofon2 8729*	Cofinality theorem for ordinals. If 𝐴 and 𝐵 are mutually cofinal, then their upper bounds agree. Compare cofcut2 27974 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝒫 On)    &   ⊢ (𝜑 → 𝐵 ∈ 𝒫 On)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤)    ⇒   ⊢ (𝜑 → ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎} = ∩ {𝑏 ∈ On ∣ 𝐵 ⊆ 𝑏})
Theorem	cofonr 8730*	Inverse cofinality law for ordinals. Contrast with cofcutr 27976 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥})    ⇒   ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧)
Theorem	naddfn 8731	Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ +no Fn (On × On)
Theorem	naddcllem 8732*	Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
Theorem	naddcl 8733	Closure law for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) ∈ On)
Theorem	naddov 8734*	The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
Theorem	naddov2 8735*	Alternate expression for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥 ∧ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)})
Theorem	naddov3 8736*	Alternate expression for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑥})
Theorem	naddf 8737	Function statement for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ +no :(On × On)⟶On
Theorem	naddcom 8738	Natural addition commutes. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = (𝐵 +no 𝐴))
Theorem	naddrid 8739	Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.)
⊢ (𝐴 ∈ On → (𝐴 +no ∅) = 𝐴)
Theorem	naddlid 8740	Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 20-Feb-2025.)
⊢ (𝐴 ∈ On → (∅ +no 𝐴) = 𝐴)
Theorem	naddssim 8741	Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 +no 𝐶) ⊆ (𝐵 +no 𝐶)))
Theorem	naddelim 8742	Ordinal less-than is preserved by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 +no 𝐶) ∈ (𝐵 +no 𝐶)))
Theorem	naddel1 8743	Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 +no 𝐶) ∈ (𝐵 +no 𝐶)))
Theorem	naddel2 8744	Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐶 +no 𝐴) ∈ (𝐶 +no 𝐵)))
Theorem	naddss1 8745	Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 +no 𝐶) ⊆ (𝐵 +no 𝐶)))
Theorem	naddss2 8746	Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +no 𝐴) ⊆ (𝐶 +no 𝐵)))
Theorem	naddword1 8747	Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 21-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +no 𝐵))
Theorem	naddword2 8748	Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 15-Feb-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐵 +no 𝐴))
Theorem	naddunif 8749*	Uniformity theorem for natural addition. If 𝐴 is the upper bound of 𝑋 and 𝐵 is the upper bound of 𝑌, then (𝐴 +no 𝐵) can be expressed in terms of 𝑋 and 𝑌. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → 𝐵 ∈ On)    &   ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥})    &   ⊢ (𝜑 → 𝐵 = ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦})    ⇒   ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧})
Theorem	naddasslem1 8750*	Lemma for naddass 8752. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = ∩ {𝑥 ∈ On ∣ (∀𝑎 ∈ 𝐴 ((𝑎 +no 𝐵) +no 𝐶) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝐵 ((𝐴 +no 𝑏) +no 𝐶) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝐶 ((𝐴 +no 𝐵) +no 𝑐) ∈ 𝑥)})
Theorem	naddasslem2 8751*	Lemma for naddass 8752. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 +no (𝐵 +no 𝐶)) = ∩ {𝑥 ∈ On ∣ (∀𝑎 ∈ 𝐴 (𝑎 +no (𝐵 +no 𝐶)) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝐵 (𝐴 +no (𝑏 +no 𝐶)) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝐶 (𝐴 +no (𝐵 +no 𝑐)) ∈ 𝑥)})
Theorem	naddass 8752	Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = (𝐴 +no (𝐵 +no 𝐶)))
Theorem	nadd32 8753	Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 20-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = ((𝐴 +no 𝐶) +no 𝐵))
Theorem	nadd4 8754	Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 +no 𝐵) +no (𝐶 +no 𝐷)) = ((𝐴 +no 𝐶) +no (𝐵 +no 𝐷)))
Theorem	nadd42 8755	Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 +no 𝐵) +no (𝐶 +no 𝐷)) = ((𝐴 +no 𝐶) +no (𝐷 +no 𝐵)))
Theorem	naddel12 8756	Natural addition to both sides of ordinal less-than. (Contributed by Scott Fenton, 7-Feb-2025.)
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 +no 𝐵) ∈ (𝐶 +no 𝐷)))
Theorem	naddsuc2 8757	Natural addition with successor. (Contributed by RP, 1-Jan-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵))
Theorem	naddoa 8758	Natural addition of a natural is the same as regular addition. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +no 𝐵) = (𝐴 +o 𝐵))
Theorem	omnaddcl 8759	The naturals are closed under natural addition. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +no 𝐵) ∈ ω)
2.4.26  Equivalence relations and classes
Syntax	wer 8760	Extend the definition of a wff to include the equivalence predicate.
wff 𝑅 Er 𝐴
Syntax	cec 8761	Extend the definition of a class to include equivalence class.
class [𝐴]𝑅
Syntax	cqs 8762	Extend the definition of a class to include quotient set.
class (𝐴 / 𝑅)
Definition	df-er 8763	Define the equivalence relation predicate. Our notation is not standard. A formal notation doesn't seem to exist in the literature; instead only informal English tends to be used. The present definition, although somewhat cryptic, nicely avoids dummy variables. In dfer2 8764 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 8783, ersymb 8777, and ertr 8778. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅))
Theorem	dfer2 8764*	Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
Definition	df-ec 8765	Define the 𝑅-coset of 𝐴. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of 𝐴 modulo 𝑅 when 𝑅 is an equivalence relation (i.e. when Er 𝑅; see dfer2 8764). In this case, 𝐴 is a representative (member) of the equivalence class [𝐴]𝑅, which contains all sets that are equivalent to 𝐴. Definition of [Enderton] p. 57 uses the notation [𝐴] (subscript) 𝑅, although we simply follow the brackets by 𝑅 since we don't have subscripted expressions. For an alternate definition, see dfec2 8766. (Contributed by NM, 23-Jul-1995.)
⊢ [𝐴]𝑅 = (𝑅 “ {𝐴})
Theorem	dfec2 8766*	Alternate definition of 𝑅-coset of 𝐴. Definition 34 of [Suppes] p. 81. (Contributed by NM, 3-Jan-1997.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → [𝐴]𝑅 = {𝑦 ∣ 𝐴𝑅𝑦})
Theorem	ecexg 8767	An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.)
⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V)
Theorem	ecexr 8768	A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ [𝐵]𝑅 → 𝐵 ∈ V)
Definition	df-qs 8769*	Define quotient set. 𝑅 is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅}
Theorem	ereq1 8770	Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴))
Theorem	ereq2 8771	Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝐴 = 𝐵 → (𝑅 Er 𝐴 ↔ 𝑅 Er 𝐵))
Theorem	errel 8772	An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → Rel 𝑅)
Theorem	erdm 8773	The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴)
Theorem	ercl 8774	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝑋)
Theorem	ersym 8775	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐴)
Theorem	ercl2 8776	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑋)
Theorem	ersymb 8777	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	ertr 8778	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Theorem	ertrd 8779	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr2d 8780	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐶𝑅𝐴)
Theorem	ertr3d 8781	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵𝑅𝐴)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr4d 8782	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	erref 8783	An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐴)
Theorem	ercnv 8784	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅)
Theorem	errn 8785	The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ran 𝑅 = 𝐴)
Theorem	erssxp 8786	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴))
Theorem	erex 8787	An equivalence relation is a set if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → (𝐴 ∈ 𝑉 → 𝑅 ∈ V))
Theorem	erexb 8788	An equivalence relation is a set if and only if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → (𝑅 ∈ V ↔ 𝐴 ∈ V))
Theorem	iserd 8789*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥)    &   ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥))    ⇒   ⊢ (𝜑 → 𝑅 Er 𝐴)
Theorem	iseri 8790*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8789, which avoids the need to provide a "dummy antecedent" 𝜑 if there is no natural one to choose. (Contributed by AV, 30-Apr-2021.)
⊢ Rel 𝑅    &   ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥)    &   ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)    &   ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)    ⇒   ⊢ 𝑅 Er 𝐴
Theorem	iseriALT 8791*	Alternate proof of iseri 8790, avoiding the usage of mptru 1544 and ⊤ as antecedent by using ax-mp 5 and one of the hypotheses as antecedent. This results, however, in a slightly longer proof. (Contributed by AV, 30-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Rel 𝑅    &   ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥)    &   ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)    &   ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)    ⇒   ⊢ 𝑅 Er 𝐴
Theorem	brinxper 8792*	Conditions for a reflexive, symmetric and transitive binary relation to be an equivalence relation over a class 𝑉. (Contributed by AV, 11-Jun-2025.)
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∼ 𝑥)    &   ⊢ (𝑥 ∈ 𝑉 → (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥))    &   ⊢ (𝑥 ∈ 𝑉 → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧))    ⇒   ⊢ ( ∼ ∩ (𝑉 × 𝑉)) Er 𝑉
Theorem	brdifun 8793	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	swoer 8794*	Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    ⇒   ⊢ (𝜑 → 𝑅 Er 𝑋)
Theorem	swoord1 8795*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
Theorem	swoord2 8796*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵))
Theorem	swoso 8797*	If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ∧ 𝑥𝑅𝑦)) → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → < Or 𝑌)
Theorem	eqerlem 8798*	Lemma for eqer 8799. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
Theorem	eqer 8799*	Equivalence relation involving equality of dependent classes 𝐴(𝑥) and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ 𝑅 Er V
Theorem	ider 8800	The identity relation is an equivalence relation. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
⊢ I Er V