P. 104 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10301-10400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zfcndrep 10301*	Axiom of Replacement ax-rep 5205, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	zfcndun 10302*	Axiom of Union ax-un 7566, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfcndpow 10303*	Axiom of Power Sets ax-pow 5283, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru 5288. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfcndreg 10304*	Axiom of Regularity ax-reg 9281, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	zfcndinf 10305*	Axiom of Infinity ax-inf 9326, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5287 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	zfcndac 10306*	Axiom of Choice ax-ac 10146, 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 10307	Extend class notation to include the collection of sets that satisfy the GCH.
class GCH
Definition	df-gch 10308*	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 10309*	Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴))))
Theorem	fingch 10310	A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ Fin ⊆ GCH
Theorem	gchi 10311	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 10312	If 𝐴 ≤ 𝐵 < 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐴 = 𝐵 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴)) → 𝐴 ≈ 𝐵)
Theorem	gchen2 10313	If 𝐴 < 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → 𝐵 ≈ 𝒫 𝐴)
Theorem	gchor 10314	If 𝐴 ≤ 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then either 𝐴 = 𝐵 or 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → (𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴))
Theorem	engch 10315	The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ GCH ↔ 𝐵 ∈ GCH))
Theorem	gchdomtri 10316	Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 10368. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴))
Theorem	fpwwe2cbv 10317*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 3-Jun-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    ⇒   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
Theorem	fpwwe2lem1 10318*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    ⇒   ⊢ 𝑊 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴))
Theorem	fpwwe2lem2 10319*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
Theorem	fpwwe2lem3 10320*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → ((◡𝑅 “ {𝐵})𝐹(𝑅 ∩ ((◡𝑅 “ {𝐵}) × (◡𝑅 “ {𝐵})))) = 𝐵)
Theorem	fpwwe2lem4 10321*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴)
Theorem	fpwwe2lem5 10322*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑁)    &   ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶)))
Theorem	fpwwe2lem6 10323*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑁)    &   ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷))))
Theorem	fpwwe2lem7 10324*	Lemma for fpwwe2 10330. 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 10325*	Lemma for fpwwe2 10330. 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 10326*	Lemma for fpwwe2 10330. 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 10327*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
Theorem	fpwwe2lem11 10328*	Lemma for fpwwe2 10330. (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 10329*	Lemma for fpwwe2 10330. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
Theorem	fpwwe2 10330*	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 9717. 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 10331*	Lemma for fpwwe 10333. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    ⇒   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))}
Theorem	fpwwelem 10332*	Lemma for fpwwe 10333. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝐹‘(◡𝑅 “ {𝑦})) = 𝑦))))
Theorem	fpwwe 10333*	Given any function 𝐹 from the powerset of 𝐴 to 𝐴, canth2 8866 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 9717. 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 10334*	An "effective" form of Cantor's theorem canth 7209. 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 10335*	Lemma for canthnum 10336. (Contributed by Mario Carneiro, 19-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    &   ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})    ⇒   ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴)
Theorem	canthnum 10336	The set of well-orderable subsets of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 8866. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ (𝒫 𝐴 ∩ dom card))
Theorem	canthwelem 10337*	Lemma for canthwe 10338. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}    &   ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    &   ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})    ⇒   ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:𝑂–1-1→𝐴)
Theorem	canthwe 10338*	The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 8866. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂)
Theorem	canthp1lem1 10339	Lemma for canthp1 10341. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
Theorem	canthp1lem2 10340*	Lemma for canthp1 10341. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝜑 → 1o ≺ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o))    &   ⊢ (𝜑 → 𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴)    &   ⊢ 𝐻 = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))    &   ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐻‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    ⇒   ⊢ ¬ 𝜑
Theorem	canthp1 10341	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 10342	The exclusion of finite sets from consideration in df-gch 10308 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 10343	An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 1o) ≈ 𝐴)
Theorem	gchinf 10344	An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝐴)
Theorem	pwfseqlem1 10345*	Lemma for pwfseq 10351. 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 10346*	Lemma for pwfseq 10351. (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 10347*	Lemma for pwfseq 10351. Using the construction 𝐷 from pwfseqlem1 10345, 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 10348*	Lemma for pwfseqlem4 10349. (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 10349*	Lemma for pwfseq 10351. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10347. Applying fpwwe2 10330 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.)
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))    &   ⊢ (𝜑 → 𝑋 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋)    &   ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥)    &   ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))})    &   ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥})))    &   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))}    &   ⊢ 𝑍 = ∪ dom 𝑊    ⇒   ⊢ ¬ 𝜑
Theorem	pwfseqlem5 10350*	Lemma for pwfseq 10351. Although in some ways pwfseqlem4 10349 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 9714. 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 9701. 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 9394), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9705). (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 10351*	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 10352	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 10353	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 10354	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 10355	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 10356	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 10357	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 10358	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 10359	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 10360	If 𝐴 + ≈ 𝒫 𝐴, then 𝐴 is a GCH-set. The much simpler converse to gchhar 10366. (Contributed by Mario Carneiro, 2-Jun-2015.)
⊢ ((har‘𝐴) ≈ 𝒫 𝐴 → 𝐴 ∈ GCH)
Theorem	alephgch 10361	If (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴), then (ℵ‘𝐴) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴) → (ℵ‘𝐴) ∈ GCH)
Theorem	gch2 10362	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 10363	An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (GCH = V ↔ ∀𝑥 ∈ On (ℵ‘suc 𝑥) ≈ 𝒫 (ℵ‘𝑥))
Theorem	gch-kn 10364*	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 10268 to the successor aleph using enen2 8854. (Contributed by NM, 1-Oct-2004.)
⊢ (𝐴 ∈ On → ((ℵ‘suc 𝐴) ≈ {𝑥 ∣ (𝑥 ⊆ (ℵ‘𝐴) ∧ 𝑥 ≈ (ℵ‘𝐴))} ↔ (ℵ‘suc 𝐴) ≈ (2o ↑m (ℵ‘𝐴))))
3.4.2  Derivation of the Axiom of Choice
Theorem	gchaclem 10365	Lemma for gchac 10368 (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝜑 → ω ≼ 𝐴)    &   ⊢ (𝜑 → 𝒫 𝐶 ∈ GCH)    &   ⊢ (𝜑 → (𝐴 ≼ 𝐶 ∧ (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))    ⇒   ⊢ (𝜑 → (𝐴 ≼ 𝒫 𝐶 ∧ (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵)))
Theorem	gchhar 10366	A "local" form of gchac 10368. 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 10367	A "local" form of gchac 10368. 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 10368	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 10510, 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 10371 and df-ina 10372 respectively ), Tarski classes (df-tsk 10436), and Grothendieck universes (df-gru 10478). We then introduce the Tarski's axiom ax-groth 10510 and prove various properties from that.
4.1  Inaccessibles
4.1.1  Weakly and strongly inaccessible cardinals
Syntax	cwina 10369	The class of weak inaccessibles.
class Inaccw
Syntax	cina 10370	The class of strong inaccessibles.
class Inacc
Definition	df-wina 10371*	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 10372*	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 10373*	Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.)
⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦))
Theorem	elina 10374*	Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.)
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴))
Theorem	winaon 10375	A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On)
Theorem	inawinalem 10376*	Lemma for inawina 10377. (Contributed by Mario Carneiro, 8-Jun-2014.)
⊢ (𝐴 ∈ On → (∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦))
Theorem	inawina 10377	Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
Theorem	omina 10378	ω is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow ω as an inaccessible cardinal, but this choice allows us to reuse our results for inaccessibles for ω.) (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ω ∈ Inacc
Theorem	winacard 10379	A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
Theorem	winainflem 10380*	A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴)
Theorem	winainf 10381	A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
Theorem	winalim 10382	A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ (𝐴 ∈ Inaccw → Lim 𝐴)
Theorem	winalim2 10383*	A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))
Theorem	winafp 10384	A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.)
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (ℵ‘𝐴) = 𝐴)
Theorem	winafpi 10385	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 4514 to turn this type of statement into the closed form statement winafp 10384, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 10384 using this theorem and dedth 4514, in ZFC. (You can prove this if you use ax-groth 10510, though.) (Contributed by Mario Carneiro, 28-May-2014.)
⊢ 𝐴 ∈ Inaccw    &   ⊢ 𝐴 ≠ ω    ⇒   ⊢ (ℵ‘𝐴) = 𝐴
Theorem	gchina 10386	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 10387	Extend class definition to include the class of all weak universes.
class WUni
Syntax	cwunm 10388	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 10389*	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 10427) whereas the analogue for Grothendieck universes requires ax-groth 10510 (see grothtsk 10522). (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ WUni = {𝑢 ∣ (Tr 𝑢 ∧ 𝑢 ≠ ∅ ∧ ∀𝑥 ∈ 𝑢 (∪ 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Definition	df-wunc 10390*	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 10391*	Properties of a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑥 ∈ 𝑈 (∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∈ 𝑈))))
Theorem	wuntr 10392	A weak universe is transitive. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝑈 ∈ WUni → Tr 𝑈)
Theorem	wununi 10393	A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝑈)
Theorem	wunpw 10394	A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈)
Theorem	wunelss 10395	The elements of a weak universe are also subsets of it. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
Theorem	wunpr 10396	A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)
Theorem	wunun 10397	A weak universe is closed under binary union. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	wuntp 10398	A weak universe is closed under unordered triple. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑈)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵, 𝐶} ∈ 𝑈)
Theorem	wunss 10399	A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ∈ 𝑈)
Theorem	wunin 10400	A weak universe is closed under binary intersections. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ∈ 𝑈)