P. 95 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9401-9500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ordiso2 9401	Generalize ordiso 9402 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Theorem	ordiso 9402*	Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.) (Proof shortened by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 = 𝐵 ↔ ∃𝑓 𝑓 Isom E , E (𝐴, 𝐵)))
Theorem	ordtypecbv 9403*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    ⇒   ⊢ recs((𝑓 ∈ V ↦ (℩𝑠 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) = 𝐹
Theorem	ordtypelem1 9404*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇))
Theorem	ordtypelem2 9405*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → Ord 𝑇)
Theorem	ordtypelem3 9406*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
Theorem	ordtypelem4 9407*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
Theorem	ordtypelem5 9408*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (Ord dom 𝑂 ∧ 𝑂:dom 𝑂⟶𝐴))
Theorem	ordtypelem6 9409*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀)))
Theorem	ordtypelem7 9410*	Lemma for ordtype 9418. ran 𝑂 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂))
Theorem	ordtypelem8 9411*	Lemma for ordtype 9418. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂))
Theorem	ordtypelem9 9412*	Lemma for ordtype 9418. Either the function OrdIso is an isomorphism onto all of 𝐴, or OrdIso is not a set, which by oif 9416 implies that either ran 𝑂 ⊆ 𝐴 is a proper class or dom 𝑂 = On. (Contributed by Mario Carneiro, 25-Jun-2015.) (Revised by AV, 28-Jul-2024.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    &   ⊢ (𝜑 → 𝑂 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
Theorem	ordtypelem10 9413*	Lemma for ordtype 9418. Using ax-rep 5217, exclude the possibility that 𝑂 is a proper class and does not enumerate all of 𝐴. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
Theorem	oi0 9414	Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (¬ (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 = ∅)
Theorem	oicl 9415	The order type of the well-order 𝑅 on 𝐴 is an ordinal. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ Ord dom 𝐹
Theorem	oif 9416	The order isomorphism of the well-order 𝑅 on 𝐴 is a function. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ 𝐹:dom 𝐹⟶𝐴
Theorem	oiiso2 9417	The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism onto ran 𝑂 (which is a subset of 𝐴 by oif 9416). (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, ran 𝐹))
Theorem	ordtype 9418	For any set-like well-ordered class, there is an isomorphic ordinal number called its order type. (Contributed by Jeff Hankins, 17-Oct-2009.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
Theorem	oiiniseg 9419	ran 𝐹 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑁 ∈ 𝐴 ∧ 𝑀 ∈ dom 𝐹)) → ((𝐹‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝐹))
Theorem	ordtype2 9420	For any set-like well-ordered class, if the order isomorphism exists (is a set), then it maps some ordinal onto 𝐴 isomorphically. Otherwise, 𝐹 is a proper class, which implies that either ran 𝐹 ⊆ 𝐴 is a proper class or dom 𝐹 = On. This weak version of ordtype 9418 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
Theorem	oiexg 9421	The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ V)
Theorem	oion 9422	The order type of the well-order 𝑅 on 𝐴 is an ordinal. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → dom 𝐹 ∈ On)
Theorem	oiiso 9423	The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
Theorem	oien 9424	The order type of a well-ordered set is equinumerous to the set. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴) → dom 𝐹 ≈ 𝐴)
Theorem	oieu 9425	Uniqueness of the unique ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ((Ord 𝐵 ∧ 𝐺 Isom E , 𝑅 (𝐵, 𝐴)) ↔ (𝐵 = dom 𝐹 ∧ 𝐺 = 𝐹)))
Theorem	oismo 9426	When 𝐴 is a subclass of On, 𝐹 is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of 𝐴). The proof avoids ax-rep 5217 (the second statement is trivial under ax-rep 5217). (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = OrdIso( E , 𝐴)    ⇒   ⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴))
Theorem	oiid 9427	The order type of an ordinal under the ∈ order is itself, and the order isomorphism is the identity function. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ (Ord 𝐴 → OrdIso( E , 𝐴) = ( I ↾ 𝐴))
Theorem	hartogslem1 9428*	Lemma for hartogs 9430. (Contributed by Mario Carneiro, 14-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}    &   ⊢ 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}    ⇒   ⊢ (dom 𝐹 ⊆ 𝒫 (𝐴 × 𝐴) ∧ Fun 𝐹 ∧ (𝐴 ∈ 𝑉 → ran 𝐹 = {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴}))
Theorem	hartogslem2 9429*	Lemma for hartogs 9430. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}    &   ⊢ 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V)
Theorem	hartogs 9430*	The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9428 and hartogslem2 9429) proof can be given using the axiom of choice, see ondomon 10451. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9443. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On)
Theorem	wofib 9431	The only sets which are well-ordered forwards and backwards are finite sets. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 23-May-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ↔ (𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴))
Theorem	wemaplem1 9432*	Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏)))))
Theorem	wemaplem2 9433*	Lemma for wemapso 9437. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)))    &   ⊢ (𝜑 → 𝑏 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐)))    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemaplem3 9434*	Lemma for wemapso 9437. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑃𝑇𝑋)    &   ⊢ (𝜑 → 𝑋𝑇𝑄)    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemappo 9435*	Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴))
Theorem	wemapsolem 9436*	Lemma for wemapso 9437. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Or 𝐵)    &   ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)    ⇒   ⊢ (𝜑 → 𝑇 Or 𝑈)
Theorem	wemapso 9437*	Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐵 ↑m 𝐴))
Theorem	wemapso2lem 9438*	Lemma for wemapso2 9439. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈)
Theorem	wemapso2 9439*	An alternative to having a well-order on 𝑅 in wemapso 9437 is to restrict the function set to finitely-supported functions. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or 𝑈)
Theorem	card2on 9440*	The alternate definition of the cardinal of a set given in cardval2 9881 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On
Theorem	card2inf 9441*	The alternate definition of the cardinal of a set given in cardval2 9881 has the curious property that for non-numerable sets (for which ndmfv 6854 yields ∅), it still evaluates to a nonempty set, and indeed it contains ω. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (¬ ∃𝑦 ∈ On 𝑦 ≈ 𝐴 → ω ⊆ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})
2.4.40  Hartogs function
Syntax	char 9442	Class symbol for the Hartogs function.
class har
Definition	df-har 9443*	Define the Hartogs function as mapping a set to the class of ordinals it dominates. That class is an ordinal by hartogs 9430, which is used in harf 9444. The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 9887 proves that the Hartogs function actually gives the Hartogs number for well-orderable sets. The Hartogs number of an ordinal is its cardinal successor. This is proved for finite ordinal in harsucnn 9888. Traditionally, the Hartogs number of a set 𝑋 is written ℵ(𝑋), and its cardinal successor, 𝑋 +; we use functional notation for this, and cannot use the aleph symbol because it is taken for the enumerating function of the infinite initial ordinals df-aleph 9830. Some authors define the Hartogs number of a set to be the least *infinite* ordinal which does not inject into it, thus causing the range to consist only of alephs. We use the simpler definition where the value can be any successor cardinal. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ har = (𝑥 ∈ V ↦ {𝑦 ∈ On ∣ 𝑦 ≼ 𝑥})
Theorem	harf 9444	Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ har:V⟶On
Theorem	harcl 9445	Values of the Hartogs function are ordinals (closure of the Hartogs function in the ordinals). (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (har‘𝑋) ∈ On
Theorem	harval 9446*	Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋})
Theorem	elharval 9447	The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl 9445, this implies that the Hartogs number of a set is greater than all ordinals that set dominates. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝑌 ∈ (har‘𝑋) ↔ (𝑌 ∈ On ∧ 𝑌 ≼ 𝑋))
Theorem	harndom 9448	The Hartogs number of a set does not inject into that set. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ ¬ (har‘𝑋) ≼ 𝑋
Theorem	harword 9449	Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.)
⊢ (𝑋 ≼ 𝑌 → (har‘𝑋) ⊆ (har‘𝑌))
2.4.41  Weak dominance
Syntax	cwdom 9450	Class symbol for the weak dominance relation.
class ≼*
Definition	df-wdom 9451*	A set is weakly dominated by a "larger" set if the "larger" set can be mapped onto the "smaller" set or the smaller set is empty, or equivalently, if the smaller set can be placed into bijection with some partition of the larger set. Dominance (df-dom 8871) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10411 proves that the axiom of choice implies the partition principle (over ZF). It is not known whether the partition principle is equivalent to the axiom of choice (over ZF), although it is know to imply dependent choice. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}
Theorem	relwdom 9452	Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ Rel ≼*
Theorem	brwdom 9453*	Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))
Theorem	brwdomi 9454*	Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≼* 𝑌 → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))
Theorem	brwdomn0 9455*	Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋))
Theorem	0wdom 9456	Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → ∅ ≼* 𝑋)
Theorem	fowdom 9457	An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼* 𝑌)
Theorem	wdomref 9458	Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋)
Theorem	brwdom2 9459*	Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋))
Theorem	domwdom 9460	Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌)
Theorem	wdomtr 9461	Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑋 ≼* 𝑍)
Theorem	wdomen1 9462	Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼* 𝐶 ↔ 𝐵 ≼* 𝐶))
Theorem	wdomen2 9463	Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵))
Theorem	wdompwdom 9464	Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≼* 𝑌 → 𝒫 𝑋 ≼ 𝒫 𝑌)
Theorem	canthwdom 9465	Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 9043, equivalent to canth 7300). (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ¬ 𝒫 𝐴 ≼* 𝐴
Theorem	wdom2d 9466*	Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 5217). (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* 𝐵)
Theorem	wdomd 9467*	Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* 𝐵)
Theorem	brwdom3 9468*	Condition for weak dominance with a condition reminiscent of wdomd 9467. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑋 ≼* 𝑌 ↔ ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦)))
Theorem	brwdom3i 9469*	Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝑋 ≼* 𝑌 → ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦))
Theorem	unwdomg 9470	Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼* (𝐵 ∪ 𝐷))
Theorem	xpwdomg 9471	Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷))
Theorem	wdomima2g 9472	A set is weakly dominant over its image under any function. This version of wdomimag 9473 is stated so as to avoid ax-rep 5217. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 “ 𝐴) ≼* 𝐴)
Theorem	wdomimag 9473	A set is weakly dominant over its image under any function. (Contributed by Stefan O'Rear, 14-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉) → (𝐹 “ 𝐴) ≼* 𝐴)
Theorem	unxpwdom2 9474	Lemma for unxpwdom 9475. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
Theorem	unxpwdom 9475	If a Cartesian product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of [KanamoriPincus] p. 420. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 × 𝐴) ≼ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
Theorem	ixpiunwdom 9476*	Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 8852 this shows that ∪ 𝑥 ∈ 𝐴𝐵 and X𝑥 ∈ 𝐴𝐵 have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈ 𝐴 𝐵 × 𝐴))
Theorem	harwdom 9477	The value of the Hartogs function at a set 𝑋 is weakly dominated by 𝒫 (𝑋 × 𝑋). This follows from a more precise analysis of the bound used in hartogs 9430 to prove that (har‘𝑋) is an ordinal. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) ≼* 𝒫 (𝑋 × 𝑋))
2.5  ZF Set Theory - add the Axiom of Regularity
2.5.1  Introduce the Axiom of Regularity
Axiom	ax-reg 9478*	Axiom of Regularity. An axiom of Zermelo-Fraenkel set theory. Also called the Axiom of Foundation. A rather non-intuitive axiom that denies more than it asserts, it states (in the form of zfreg 9482) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9483). A stronger version that works for proper classes is proved as zfregs 9622. (Contributed by NM, 14-Aug-1993.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	axreg2 9479*	Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.)
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	zfregcl 9480*	The Axiom of Regularity with class variables. (Contributed by NM, 5-Aug-1994.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) Avoid ax-10 2144 and ax-12 2180. (Revised by TM, 31-Dec-2025.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴))
Theorem	zfregclOLD 9481*	Obsolete version of zfregcl 9480 as of 31-Dec-2025. (Contributed by NM, 5-Aug-1994.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴))
Theorem	zfreg 9482*	The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the "weak form". Axiom Reg of [BellMachover] p. 480. There is also a "strong form", not requiring that 𝐴 be a set, that can be proved with more difficulty (see zfregs 9622). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	elirrv 9483	The membership relation is irreflexive: no set is a member of itself. Theorem 105 of [Suppes] p. 54. This is trivial to prove from zfregfr 9494 and efrirr 5596 (see elirrvALT 9495), but this proof is direct from ax-reg 9478. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9478 directly. (Revised by BTernaryTau, 27-Dec-2025.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirrvOLD 9484	Obsolete version of elirrv 9483 as of 27-Dec-2025. (Contributed by NM, 19-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirr 9485	No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. Theorem 1.9(i) of [Schloeder] p. 1. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ¬ 𝐴 ∈ 𝐴
Theorem	elneq 9486	A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ≠ 𝐵)
Theorem	nelaneq 9487	A class is not an element of and equal to a class at the same time. Variant of elneq 9486 analogously to elnotel 9500 and en2lp 9496. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof shortened by TM, 31-Dec-2025.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	nelaneqOLD 9488	Obsolete version of nelaneq 9487 as of 31-Dec-2025. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	epinid0 9489	The membership relation and the identity relation are disjoint. Variable-free version of nelaneq 9487. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.)
⊢ ( E ∩ I ) = ∅
Theorem	sucprcreg 9490	A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004.) (Proof shortened by BJ, 16-Apr-2019.)
⊢ (¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴)
Theorem	ruv 9491	The Russell class is equal to the universe V. Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} = V
Theorem	ruALT 9492	Alternate proof of ru 3739, simplified using (indirectly) the Axiom of Regularity ax-reg 9478. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V
Theorem	disjcsn 9493	A class is disjoint from its singleton. A consequence of regularity. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by BJ, 4-Apr-2019.)
⊢ (𝐴 ∩ {𝐴}) = ∅
Theorem	zfregfr 9494	The membership relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.)
⊢ E Fr 𝐴
Theorem	elirrvALT 9495	Alternate proof of elirrv 9483, shorter but using more axioms. (Contributed by BTernaryTau, 28-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	en2lp 9496	No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton] p. 206. (Contributed by NM, 16-Oct-1996.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴)
Theorem	elnanel 9497	Two classes are not elements of each other simultaneously. This is just a rewriting of en2lp 9496 and serves as an example in the context of Godel codes, see elnanelprv 35461. (Contributed by AV, 5-Nov-2023.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 ⊼ 𝐵 ∈ 𝐴)
Theorem	cnvepnep 9498	The membership (epsilon) relation and its converse are disjoint, i.e., E is an asymmetric relation. Variable-free version of en2lp 9496. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 19-Jun-2022.)
⊢ (◡ E ∩ E ) = ∅
Theorem	epnsym 9499	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ◡ E ≠ E
Theorem	elnotel 9500	A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴)