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	infiso 9401*	Image of an infimum under an isomorphism. (Contributed by AV, 4-Sep-2020.)
⊢ (𝜑 → 𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵))    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐶 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → ∃𝑧 ∈ 𝐶 𝑧𝑅𝑦)))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → inf((𝐹 “ 𝐶), 𝐵, 𝑆) = (𝐹‘inf(𝐶, 𝐴, 𝑅)))
2.4.39  Ordinal isomorphism, Hartogs's theorem
Syntax	coi 9402	Extend class definition to include the canonical order isomorphism to an ordinal.
class OrdIso(𝑅, 𝐴)
Definition	df-oi 9403*	Define the canonical order isomorphism from the well-order 𝑅 on 𝐴 to an ordinal. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (recs((ℎ ∈ V ↦ (℩𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
Theorem	dfoi 9404*	Rewrite df-oi 9403 with abbreviations. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴), (𝐹 ↾ {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}), ∅)
Theorem	oieq1 9405	Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ (𝑅 = 𝑆 → OrdIso(𝑅, 𝐴) = OrdIso(𝑆, 𝐴))
Theorem	oieq2 9406	Equality theorem for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ (𝐴 = 𝐵 → OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐵))
Theorem	nfoi 9407	Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥OrdIso(𝑅, 𝐴)
Theorem	ordiso2 9408	Generalize ordiso 9409 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Theorem	ordiso 9409*	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 9410*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    ⇒   ⊢ recs((𝑓 ∈ V ↦ (℩𝑠 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) = 𝐹
Theorem	ordtypelem1 9411*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇))
Theorem	ordtypelem2 9412*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → Ord 𝑇)
Theorem	ordtypelem3 9413*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑀) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
Theorem	ordtypelem4 9414*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
Theorem	ordtypelem5 9415*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → (Ord dom 𝑂 ∧ 𝑂:dom 𝑂⟶𝐴))
Theorem	ordtypelem6 9416*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ 𝑀 → (𝑂‘𝑁)𝑅(𝑂‘𝑀)))
Theorem	ordtypelem7 9417*	Lemma for ordtype 9425. 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 9418*	Lemma for ordtype 9425. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}    &   ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))    &   ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}    &   ⊢ 𝑂 = OrdIso(𝑅, 𝐴)    &   ⊢ (𝜑 → 𝑅 We 𝐴)    &   ⊢ (𝜑 → 𝑅 Se 𝐴)    ⇒   ⊢ (𝜑 → 𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂))
Theorem	ordtypelem9 9419*	Lemma for ordtype 9425. Either the function OrdIso is an isomorphism onto all of 𝐴, or OrdIso is not a set, which by oif 9423 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 9420*	Lemma for ordtype 9425. Using ax-rep 5219, 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 9421	Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (¬ (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 = ∅)
Theorem	oicl 9422	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 9423	The order isomorphism of the well-order 𝑅 on 𝐴 is a function. (Contributed by Mario Carneiro, 23-May-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ 𝐹:dom 𝐹⟶𝐴
Theorem	oiiso2 9424	The order isomorphism of the well-order 𝑅 on 𝐴 is an isomorphism onto ran 𝑂 (which is a subset of 𝐴 by oif 9423). (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Isom E , 𝑅 (dom 𝐹, ran 𝐹))
Theorem	ordtype 9425	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 9426	ran 𝐹 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑁 ∈ 𝐴 ∧ 𝑀 ∈ dom 𝐹)) → ((𝐹‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝐹))
Theorem	ordtype2 9427	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 9425 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V) → 𝐹 Isom E , 𝑅 (dom 𝐹, 𝐴))
Theorem	oiexg 9428	The order isomorphism on a set is a set. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ 𝐹 = OrdIso(𝑅, 𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐹 ∈ V)
Theorem	oion 9429	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 9430	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 9431	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 9432	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 9433	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 5219 (the second statement is trivial under ax-rep 5219). (Contributed by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐹 = OrdIso( E , 𝐴)    ⇒   ⊢ (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴))
Theorem	oiid 9434	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 9435*	Lemma for hartogs 9437. (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 9436*	Lemma for hartogs 9437. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ 𝐹 = {⟨𝑟, 𝑦⟩ ∣ (((dom 𝑟 ⊆ 𝐴 ∧ ( I ↾ dom 𝑟) ⊆ 𝑟 ∧ 𝑟 ⊆ (dom 𝑟 × dom 𝑟)) ∧ (𝑟 ∖ I ) We dom 𝑟) ∧ 𝑦 = dom OrdIso((𝑟 ∖ I ), dom 𝑟))}    &   ⊢ 𝑅 = {⟨𝑠, 𝑡⟩ ∣ ∃𝑤 ∈ 𝑦 ∃𝑧 ∈ 𝑦 ((𝑠 = (𝑓‘𝑤) ∧ 𝑡 = (𝑓‘𝑧)) ∧ 𝑤 E 𝑧)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ V)
Theorem	hartogs 9437*	The class of ordinals dominated by a given set is an ordinal. A shorter (when taking into account lemmas hartogslem1 9435 and hartogslem2 9436) proof can be given using the axiom of choice, see ondomon 10461. As its label indicates, this result is used to justify the definition of the Hartogs function df-har 9450. (Contributed by Jeff Hankins, 22-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On)
Theorem	wofib 9438	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 9439*	Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    ⇒   ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏)))))
Theorem	wemaplem2 9440*	Lemma for wemapso 9444. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑎 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑃‘𝑎)𝑆(𝑋‘𝑎))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑎 → (𝑃‘𝑐) = (𝑋‘𝑐)))    &   ⊢ (𝜑 → 𝑏 ∈ 𝐴)    &   ⊢ (𝜑 → (𝑋‘𝑏)𝑆(𝑄‘𝑏))    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝑋‘𝑐) = (𝑄‘𝑐)))    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemaplem3 9441*	Lemma for wemapso 9444. Transitivity. (Contributed by Stefan O'Rear, 17-Jan-2015.) (Revised by AV, 21-Jul-2024.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ (𝜑 → 𝑃 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑋 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑄 ∈ (𝐵 ↑m 𝐴))    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → 𝑆 Po 𝐵)    &   ⊢ (𝜑 → 𝑃𝑇𝑋)    &   ⊢ (𝜑 → 𝑋𝑇𝑄)    ⇒   ⊢ (𝜑 → 𝑃𝑇𝑄)
Theorem	wemappo 9442*	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 9443*	Lemma for wemapso 9444. (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 9444*	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 9445*	Lemma for wemapso2 9446. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 1-Jul-2019.)
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}    &   ⊢ 𝑈 = {𝑥 ∈ (𝐵 ↑m 𝐴) ∣ 𝑥 finSupp 𝑍}    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) ∧ 𝑍 ∈ 𝑊) → 𝑇 Or 𝑈)
Theorem	wemapso2 9446*	An alternative to having a well-order on 𝑅 in wemapso 9444 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 9447*	The alternate definition of the cardinal of a set given in cardval2 9891 always gives a set, and indeed an ordinal. (Contributed by Mario Carneiro, 14-Jan-2013.)
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On
Theorem	card2inf 9448*	The alternate definition of the cardinal of a set given in cardval2 9891 has the curious property that for non-numerable sets (for which ndmfv 6860 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 9449	Class symbol for the Hartogs function.
class har
Definition	df-har 9450*	Define the Hartogs function as mapping a set to the class of ordinals it dominates. That class is an ordinal by hartogs 9437, which is used in harf 9451. The Hartogs number of a set is the least ordinal not dominated by that set. Theorem harval2 9897 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 9898. 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 9840. 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 9451	Functionality of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ har:V⟶On
Theorem	harcl 9452	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 9453*	Function value of the Hartogs function. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → (har‘𝑋) = {𝑦 ∈ On ∣ 𝑦 ≼ 𝑋})
Theorem	elharval 9454	The Hartogs number of a set contains exactly the ordinals that set dominates. Combined with harcl 9452, 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 9455	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 9456	Weak ordering property of the Hartogs function. (Contributed by Stefan O'Rear, 14-Feb-2015.)
⊢ (𝑋 ≼ 𝑌 → (har‘𝑋) ⊆ (har‘𝑌))
2.4.41  Weak dominance
Syntax	cwdom 9457	Class symbol for the weak dominance relation.
class ≼*
Definition	df-wdom 9458*	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 8877) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10421 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 9459	Weak dominance is a relation. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ Rel ≼*
Theorem	brwdom 9460*	Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))
Theorem	brwdomi 9461*	Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≼* 𝑌 → (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))
Theorem	brwdomn0 9462*	Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋))
Theorem	0wdom 9463	Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → ∅ ≼* 𝑋)
Theorem	fowdom 9464	An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝑌–onto→𝑋) → 𝑋 ≼* 𝑌)
Theorem	wdomref 9465	Reflexivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ∈ 𝑉 → 𝑋 ≼* 𝑋)
Theorem	brwdom2 9466*	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 9467	Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015.)
⊢ (𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌)
Theorem	wdomtr 9468	Transitivity of weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ ((𝑋 ≼* 𝑌 ∧ 𝑌 ≼* 𝑍) → 𝑋 ≼* 𝑍)
Theorem	wdomen1 9469	Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼* 𝐶 ↔ 𝐵 ≼* 𝐶))
Theorem	wdomen2 9470	Equality-like theorem for equinumerosity and weak dominance. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼* 𝐴 ↔ 𝐶 ≼* 𝐵))
Theorem	wdompwdom 9471	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 9472	Cantor's Theorem, stated using weak dominance (this is actually a stronger statement than canth2 9050, equivalent to canth 7306). (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ¬ 𝒫 𝐴 ≼* 𝐴
Theorem	wdom2d 9473*	Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 5219). (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* 𝐵)
Theorem	wdomd 9474*	Deduce weak dominance from an implicit onto function. (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐵 𝑥 = 𝑋)    ⇒   ⊢ (𝜑 → 𝐴 ≼* 𝐵)
Theorem	brwdom3 9475*	Condition for weak dominance with a condition reminiscent of wdomd 9474. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑋 ≼* 𝑌 ↔ ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦)))
Theorem	brwdom3i 9476*	Weak dominance implies existence of a covering function. (Contributed by Stefan O'Rear, 13-Feb-2015.)
⊢ (𝑋 ≼* 𝑌 → ∃𝑓∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝑥 = (𝑓‘𝑦))
Theorem	unwdomg 9477	Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼* (𝐵 ∪ 𝐷))
Theorem	xpwdomg 9478	Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷))
Theorem	wdomima2g 9479	A set is weakly dominant over its image under any function. This version of wdomimag 9480 is stated so as to avoid ax-rep 5219. (Contributed by Mario Carneiro, 25-Jun-2015.)
⊢ ((Fun 𝐹 ∧ 𝐴 ∈ 𝑉 ∧ (𝐹 “ 𝐴) ∈ 𝑊) → (𝐹 “ 𝐴) ≼* 𝐴)
Theorem	wdomimag 9480	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 9481	Lemma for unxpwdom 9482. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))
Theorem	unxpwdom 9482	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 9483*	Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg 8858 this shows that ∪ 𝑥 ∈ 𝐴𝐵 and X𝑥 ∈ 𝐴𝐵 have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈ 𝐴 𝐵 × 𝐴))
Theorem	harwdom 9484	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 9437 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 9485*	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 9489) that every nonempty set contains a set disjoint from itself. One consequence is that it denies the existence of a set containing itself (elirrv 9490). A stronger version that works for proper classes is proved as zfregs 9629. (Contributed by NM, 14-Aug-1993.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	axreg2 9486*	Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003.)
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	zfregcl 9487*	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 2146 and ax-12 2182. (Revised by TM, 31-Dec-2025.)
⊢ (𝐴 ∈ 𝑉 → (∃𝑥 𝑥 ∈ 𝐴 → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝐴))
Theorem	zfregclOLD 9488*	Obsolete version of zfregcl 9487 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 9489*	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 9629). (Contributed by NM, 26-Nov-1995.) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	elirrv 9490	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 9501 and efrirr 5599 (see elirrvALT 9502), but this proof is direct from ax-reg 9485. (Contributed by NM, 19-Aug-1993.) Reduce axiom dependencies and make use of ax-reg 9485 directly. (Revised by BTernaryTau, 27-Dec-2025.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirrvOLD 9491	Obsolete version of elirrv 9490 as of 27-Dec-2025. (Contributed by NM, 19-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝑥 ∈ 𝑥
Theorem	elirr 9492	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 9493	A class is not equal to any of its elements. (Contributed by AV, 14-Jun-2022.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ≠ 𝐵)
Theorem	nelaneq 9494	A class is not an element of and equal to a class at the same time. Variant of elneq 9493 analogously to elnotel 9507 and en2lp 9503. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.) (Proof shortened by TM, 31-Dec-2025.)
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐴 = 𝐵)
Theorem	nelaneqOLD 9495	Obsolete version of nelaneq 9494 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 9496	The membership relation and the identity relation are disjoint. Variable-free version of nelaneq 9494. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022.)
⊢ ( E ∩ I ) = ∅
Theorem	sucprcreg 9497	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 9498	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 9499	Alternate proof of ru 3735, simplified using (indirectly) the Axiom of Regularity ax-reg 9485. (Contributed by Alan Sare, 4-Oct-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V
Theorem	disjcsn 9500	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.)
⊢ (𝐴 ∩ {𝐴}) = ∅