P. 107 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10601-10700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axacndlem4 10601*	Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)
⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
Theorem	axacndlem5 10602*	Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)
⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
Theorem	axacnd 10603	A version of the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)
⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
Theorem	zfcndext 10604*	Axiom of Extensionality ax-ext 2734, reproved from conditionless ZFC version and predicate calculus. Usage of this theorem is discouraged because it depends on ax-13 2403. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	zfcndrep 10605*	Axiom of Replacement ax-rep 5237, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2403. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	zfcndun 10606*	Axiom of Union ax-un 7734, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2403. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfcndpow 10607*	Axiom of Power Sets ax-pow 5335, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru 5417. Usage of this theorem is discouraged because it depends on ax-13 2403. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfcndreg 10608*	Axiom of Regularity ax-reg 9552, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2403. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	zfcndinf 10609*	Axiom of Infinity ax-inf 9605, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5418 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	zfcndac 10610*	Axiom of Choice ax-ac 10449, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣))
3.4  The Generalized Continuum Hypothesis
3.4.1  Sets satisfying the Generalized Continuum Hypothesis
Syntax	cgch 10611	Extend class notation to include the collection of sets that satisfy the GCH.
class GCH
Definition	df-gch 10612*	Define the collection of "GCH-sets", or sets for which the generalized continuum hypothesis holds. In this language the generalized continuum hypothesis can be expressed as GCH = V. A set 𝑥 satisfies the generalized continuum hypothesis if it is finite or there is no set 𝑦 strictly between 𝑥 and its powerset in cardinality. The continuum hypothesis is equivalent to ω ∈ GCH. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)})
Theorem	elgch 10613*	Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴))))
Theorem	fingch 10614	A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ Fin ⊆ GCH
Theorem	gchi 10615	The only GCH-sets which have other sets between it and its power set are finite sets. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴) → 𝐴 ∈ Fin)
Theorem	gchen1 10616	If 𝐴 ≤ 𝐵 < 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐴 = 𝐵 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴)) → 𝐴 ≈ 𝐵)
Theorem	gchen2 10617	If 𝐴 < 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → 𝐵 ≈ 𝒫 𝐴)
Theorem	gchor 10618	If 𝐴 ≤ 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then either 𝐴 = 𝐵 or 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → (𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴))
Theorem	engch 10619	The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ GCH ↔ 𝐵 ∈ GCH))
Theorem	gchdomtri 10620	Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 10672. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴))
Theorem	fpwwe2cbv 10621*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 3-Jun-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    ⇒   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
Theorem	fpwwe2lem1 10622*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    ⇒   ⊢ 𝑊 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴))
Theorem	fpwwe2lem2 10623*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
Theorem	fpwwe2lem3 10624*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → ((◡𝑅 “ {𝐵})𝐹(𝑅 ∩ ((◡𝑅 “ {𝐵}) × (◡𝑅 “ {𝐵})))) = 𝐵)
Theorem	fpwwe2lem4 10625*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) (Proof shortened by Matthew House, 10-Sep-2025.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴)
Theorem	fpwwe2lem5 10626*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑁)    &   ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶)))
Theorem	fpwwe2lem6 10627*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑁)    &   ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷))))
Theorem	fpwwe2lem7 10628*	Lemma for fpwwe2 10634. Show by induction that the two isometries 𝑀 and 𝑁 agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁)    ⇒   ⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀))
Theorem	fpwwe2lem8 10629*	Lemma for fpwwe2 10634. Given two well-orders ⟨𝑋, 𝑅⟩ and ⟨𝑌, 𝑆⟩ of parts of 𝐴, one is an initial segment of the other. (The 𝑂 ⊆ 𝑃 hypothesis is in order to break the symmetry of 𝑋 and 𝑌.) (Contributed by Mario Carneiro, 15-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁)    ⇒   ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Theorem	fpwwe2lem9 10630*	Lemma for fpwwe2 10634. Given two well-orders ⟨𝑋, 𝑅⟩ and ⟨𝑌, 𝑆⟩ of parts of 𝐴, one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    ⇒   ⊢ (𝜑 → ((𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) ∨ (𝑌 ⊆ 𝑋 ∧ 𝑆 = (𝑅 ∩ (𝑋 × 𝑌)))))
Theorem	fpwwe2lem10 10631*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
Theorem	fpwwe2lem11 10632*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 18-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → 𝑋 ∈ dom 𝑊)
Theorem	fpwwe2lem12 10633*	Lemma for fpwwe2 10634. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
Theorem	fpwwe2 10634*	Given any function 𝐹 from well-orderings of subsets of 𝐴 to 𝐴, there is a unique well-ordered subset ⟨𝑋, (𝑊‘𝑋)⟩ which "agrees" with 𝐹 in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 10021. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))
Theorem	fpwwecbv 10635*	Lemma for fpwwe 10637. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    ⇒   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))}
Theorem	fpwwelem 10636*	Lemma for fpwwe 10637. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝐹‘(◡𝑅 “ {𝑦})) = 𝑦))))
Theorem	fpwwe 10637*	Given any function 𝐹 from the powerset of 𝐴 to 𝐴, canth2 9116 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset ⟨𝑋, (𝑊‘𝑋)⟩ which "agrees" with 𝐹 in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 10021. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝐹‘𝑌) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋))))
Theorem	canth4 10638*	An "effective" form of Cantor's theorem canth 7366. For any function 𝐹 from the powerset of 𝐴 to 𝐴, there are two definable sets 𝐵 and 𝐶 which witness non-injectivity of 𝐹. Corollary 1.3 of [KanamoriPincus] p. 416. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    &   ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶)))
Theorem	canthnumlem 10639*	Lemma for canthnum 10640. (Contributed by Mario Carneiro, 19-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    &   ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})    ⇒   ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴)
Theorem	canthnum 10640	The set of well-orderable subsets of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 9116. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ (𝒫 𝐴 ∩ dom card))
Theorem	canthwelem 10641*	Lemma for canthwe 10642. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}    &   ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    &   ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})    ⇒   ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:𝑂–1-1→𝐴)
Theorem	canthwe 10642*	The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 9116. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂)
Theorem	canthp1lem1 10643	Lemma for canthp1 10645. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
Theorem	canthp1lem2 10644*	Lemma for canthp1 10645. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝜑 → 1o ≺ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o))    &   ⊢ (𝜑 → 𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴)    &   ⊢ 𝐻 = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))    &   ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐻‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    ⇒   ⊢ ¬ 𝜑
Theorem	canthp1 10645	A slightly stronger form of Cantor's theorem: For 1 < 𝑛, 𝑛 + 1 < 2↑𝑛. Corollary 1.6 of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (1o ≺ 𝐴 → (𝐴 ⊔ 1o) ≺ 𝒫 𝐴)
Theorem	finngch 10646	The exclusion of finite sets from consideration in df-gch 10612 is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015.)
⊢ ((𝐴 ∈ Fin ∧ 1o ≺ 𝐴) → (𝐴 ≺ (𝐴 ⊔ 1o) ∧ (𝐴 ⊔ 1o) ≺ 𝒫 𝐴))
Theorem	gchdju1 10647	An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 1o) ≈ 𝐴)
Theorem	gchinf 10648	An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝐴)
Theorem	pwfseqlem1 10649*	Lemma for pwfseq 10655. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)    &   ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)    &   ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ (∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∖ ∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)))
Theorem	pwfseqlem2 10650*	Lemma for pwfseq 10655. (Contributed by Mario Carneiro, 18-Nov-2014.) (Revised by AV, 18-Sep-2021.)
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)    &   ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)    &   ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})    &   ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))    ⇒   ⊢ ((𝑌 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑌𝐹𝑅) = (𝐻‘(card‘𝑌)))
Theorem	pwfseqlem3 10651*	Lemma for pwfseq 10655. Using the construction 𝐷 from pwfseqlem1 10649, produce a function 𝐹 that maps any well-ordered infinite set to an element outside the set. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)    &   ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)    &   ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})    &   ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥))
Theorem	pwfseqlem4a 10652*	Lemma for pwfseqlem4 10653. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)    &   ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)    &   ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})    &   ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))    ⇒   ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴)
Theorem	pwfseqlem4 10653*	Lemma for pwfseq 10655. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10651. Applying fpwwe2 10634 to it, we get a certain maximal well-ordered subset 𝑍, but the defining property (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 contradicts our assumption on 𝐹, so we are reduced to the case of 𝑍 finite. This too is a contradiction, though, because 𝑍 and its preimage under (𝑊‘𝑍) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by Matthew House, 10-Sep-2025.)
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)    &   ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)    &   ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})    &   ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))    &   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))}    &   ⊢ 𝑍 = ∪ dom 𝑊    ⇒   ⊢ ¬ 𝜑
Theorem	pwfseqlem5 10654*	Lemma for pwfseq 10655. Although in some ways pwfseqlem4 10653 is the "main" part of the proof, one last aspect which makes up a remark in the original text is by far the hardest part to formalize. The main proof relies on the existence of an injection 𝐾 from the set of finite sequences on an infinite set 𝑥 to 𝑥. Now this alone would not be difficult to prove; this is mostly the claim of fseqen 10018. However, what is needed for the proof is a canonical injection on these sets, so we have to start from scratch pulling together explicit bijections from the lemmas. If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen 10005. The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms (cnfcom3c 9673), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10009). (Contributed by Mario Carneiro, 31-May-2015.)
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)    &   ⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡))    &   ⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))    &   ⊢ 𝑂 = OrdIso(𝑟, 𝑡)    &   ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ ⟨(𝑂‘𝑢), (𝑂‘𝑣)⟩)    &   ⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇)    &   ⊢ 𝑆 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {⟨∅, (𝑂‘∅)⟩})    &   ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛) ↦ ⟨dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)⟩)    &   ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)    &   ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)    ⇒   ⊢ ¬ 𝜑
Theorem	pwfseq 10655*	The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of [KanamoriPincus] p. 418. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))
Theorem	pwxpndom2 10656	The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by AV, 18-Jul-2022.)
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 ⊔ (𝐴 × 𝐴)))
Theorem	pwxpndom 10657	The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 × 𝐴))
Theorem	pwdjundom 10658	The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 ⊔ 𝐴))
Theorem	gchdjuidm 10659	An infinite GCH-set is idempotent under cardinal sum. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴)
Theorem	gchxpidm 10660	An infinite GCH-set is idempotent under cardinal product. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴)
Theorem	gchpwdom 10661	A relationship between dominance over the powerset and strict dominance when the sets involved are infinite GCH-sets. Proposition 3.1 of [KanamoriPincus] p. 421. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴 ≺ 𝐵 ↔ 𝒫 𝐴 ≼ 𝐵))
Theorem	gchaleph 10662	If (ℵ‘𝐴) is a GCH-set and its powerset is well-orderable, then the successor aleph (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴). (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ On ∧ (ℵ‘𝐴) ∈ GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴))
Theorem	gchaleph2 10663	If (ℵ‘𝐴) and (ℵ‘suc 𝐴) are GCH-sets, then the successor aleph (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴). (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((𝐴 ∈ On ∧ (ℵ‘𝐴) ∈ GCH ∧ (ℵ‘suc 𝐴) ∈ GCH) → (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴))
Theorem	hargch 10664	If 𝐴 + ≈ 𝒫 𝐴, then 𝐴 is a GCH-set. The much simpler converse to gchhar 10670. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ ((har‘𝐴) ≈ 𝒫 𝐴 → 𝐴 ∈ GCH)
Theorem	alephgch 10665	If (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴), then (ℵ‘𝐴) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴) → (ℵ‘𝐴) ∈ GCH)
Theorem	gch2 10666	It is sufficient to require that all alephs are GCH-sets to ensure the full generalized continuum hypothesis. (The proof uses the Axiom of Regularity.) (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (GCH = V ↔ ran ℵ ⊆ GCH)
Theorem	gch3 10667	An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (GCH = V ↔ ∀𝑥 ∈ On (ℵ‘suc 𝑥) ≈ 𝒫 (ℵ‘𝑥))
Theorem	gch-kn 10668*	The equivalence of two versions of the Generalized Continuum Hypothesis. The right-hand side is the standard version in the literature. The left-hand side is a version devised by Kannan Nambiar, which he calls the Axiom of Combinatorial Sets. For the notation and motivation behind this axiom, see his paper, "Derivation of Continuum Hypothesis from Axiom of Combinatorial Sets", available at http://www.e-atheneum.net/science/derivation_ch.pdf. The equivalence of the two sides provides a negative answer to Open Problem 2 in http://www.e-atheneum.net/science/open_problem_print.pdf. The key idea in the proof below is to equate both sides of alephexp2 10572 to the successor aleph using enen2 9104. (Contributed by NM, 1-Oct-2004.)
⊢ (𝐴 ∈ On → ((ℵ‘suc 𝐴) ≈ {𝑥 ∣ (𝑥 ⊆ (ℵ‘𝐴) ∧ 𝑥 ≈ (ℵ‘𝐴))} ↔ (ℵ‘suc 𝐴) ≈ (2o ↑m (ℵ‘𝐴))))
3.4.2  Derivation of the Axiom of Choice
Theorem	gchaclem 10669	Lemma for gchac 10672 (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝜑 → ω ≼ 𝐴)    &   ⊢ (𝜑 → 𝒫 𝐶 ∈ GCH)    &   ⊢ (𝜑 → (𝐴 ≼ 𝐶 ∧ (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))    ⇒   ⊢ (𝜑 → (𝐴 ≼ 𝒫 𝐶 ∧ (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))
Theorem	gchhar 10670	A "local" form of gchac 10672. If 𝐴 and 𝒫 𝐴 are GCH-sets, then the Hartogs number of 𝐴 is 𝒫 𝐴 (so 𝒫 𝐴 and a fortiori 𝐴 are well-orderable). The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≈ 𝒫 𝐴)
Theorem	gchacg 10671	A "local" form of gchac 10672. If 𝐴 and 𝒫 𝐴 are GCH-sets, then 𝒫 𝐴 is well-orderable. The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ∈ dom card)
Theorem	gchac 10672	The Generalized Continuum Hypothesis implies the Axiom of Choice. The original proof is due to Sierpiński (1947); we use a refinement of Sierpiński's result due to Specker. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (GCH = V → CHOICE)
PART 4  TG (TARSKI-GROTHENDIECK) SET THEORY Here we introduce Tarski-Grothendieck (TG) set theory, named after mathematicians Alfred Tarski and Alexander Grothendieck. TG theory extends ZFC with the TG Axiom ax-groth 10814, which states that for every set 𝑥 there is an inaccessible cardinal 𝑦 such that 𝑦 is not in 𝑥. The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics". We first introduce the concept of inaccessibles, including weakly and strongly inaccessible cardinals (df-wina 10675 and df-ina 10676 respectively ), Tarski classes (df-tsk 10740), and Grothendieck universes (df-gru 10782). We then introduce the Tarski's axiom ax-groth 10814 and prove various properties from that.
4.1  Inaccessibles
4.1.1  Weakly and strongly inaccessible cardinals
Syntax	cwina 10673	The class of weak inaccessibles.
class Inaccw
Syntax	cina 10674	The class of strong inaccessibles.
class Inacc
Definition	df-wina 10675*	An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows ω as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013.)
⊢ Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)}
Definition	df-ina 10676*	An ordinal is strongly inaccessible iff it is a regular strong limit cardinal, which is to say that it dominates the powersets of every smaller ordinal. (Contributed by Mario Carneiro, 22-Jun-2013.)
⊢ Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)}
Theorem	elwina 10677*	Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.)
⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦))
Theorem	elina 10678*	Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.)
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴))
Theorem	winaon 10679	A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
Theorem	inawinalem 10680*	Lemma for inawina 10681. (Contributed by Mario Carneiro, 8-Jun-2014.)
⊢ (𝐴 ∈ On → (∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦))
Theorem	inawina 10681	Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
Theorem	omina 10682	ω is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow ω as an inaccessible cardinal, but this choice allows to reuse our results for inaccessibles for ω.) (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ω ∈ Inacc
Theorem	winacard 10683	A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
Theorem	winainflem 10684*	A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴)
Theorem	winainf 10685	A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
Theorem	winalim 10686	A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → Lim 𝐴)
Theorem	winalim2 10687*	A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))
Theorem	winafp 10688	A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (ℵ‘𝐴) = 𝐴)
Theorem	winafpi 10689	This theorem, which states that a nontrivial inaccessible cardinal is its own aleph number, is stated here in inference form, where the assumptions are in the hypotheses rather than an antecedent. Often, we use dedth 4545 to turn this type of statement into the closed form statement winafp 10688, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 10688 using this theorem and dedth 4545, in ZFC. (You can prove this if you use ax-groth 10814, though.) (Contributed by Mario Carneiro, 28-May-2014.)
⊢ 𝐴 ∈ Inaccw    &   ⊢ 𝐴 ≠ ω    ⇒   ⊢ (ℵ‘𝐴) = 𝐴
Theorem	gchina 10690	Assuming the GCH, weakly and strongly inaccessible cardinals coincide. Theorem 11.20 of [TakeutiZaring] p. 106. (Contributed by Mario Carneiro, 5-Jun-2015.)
⊢ (GCH = V → Inaccw = Inacc)
4.1.2  Weak universes
Syntax	cwun 10691	Extend class definition to include the class of all weak universes.
class WUni
Syntax	cwunm 10692	Extend class definition to include the map whose value is the smallest weak universe of which the given set is a subset.
class wUniCl
Definition	df-wun 10693*	The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of weak universes over Grothendieck universes is that one can prove that every set is contained in a weak universe in ZF (see uniwun 10731) whereas the analogue for Grothendieck universes requires ax-groth 10814 (see grothtsk 10826). (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Definition	df-wunc 10694*	A function that maps a set 𝑥 to the smallest weak universe that contains the elements of the set. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ wUniCl = (𝑥 ∈ V ↦ ∩ {𝑢 ∈ WUni ∣ 𝑥 ⊆ 𝑢})
Theorem	iswun 10695*	Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))))
Theorem	wuntr 10696	A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ WUni → Tr 𝑈)
Theorem	wununi 10697	A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈)
Theorem	wunpw 10698	A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
Theorem	wunelss 10699	The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
Theorem	wunpr 10700	A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)