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	cardmin 10601*	The smallest ordinal that strictly dominates a set is a cardinal. (Contributed by NM, 28-Oct-2003.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (card‘∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥})
Theorem	ficard 10602	A set is finite iff its cardinal is a natural number. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (card‘𝐴) ∈ ω))
Theorem	infinf 10603	Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017.)
⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴))
Theorem	unirnfdomd 10604	The union of the range of a function from an infinite set into the class of finite sets is dominated by its domain. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐹:𝑇⟶Fin)    &   ⊢ (𝜑 → ¬ 𝑇 ∈ Fin)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ ran 𝐹 ≼ 𝑇)
Theorem	konigthlem 10605*	Lemma for konigth 10606. (Contributed by Mario Carneiro, 22-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖)    &   ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖)    &   ⊢ 𝐷 = (𝑖 ∈ 𝐴 ↦ (𝑎 ∈ (𝑀‘𝑖) ↦ ((𝑓‘𝑎)‘𝑖)))    &   ⊢ 𝐸 = (𝑖 ∈ 𝐴 ↦ (𝑒‘𝑖))    ⇒   ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃)
Theorem	konigth 10606*	Konig's Theorem. If 𝑚(𝑖) ≺ 𝑛(𝑖) for all 𝑖 ∈ 𝐴, then Σ𝑖 ∈ 𝐴𝑚(𝑖) ≺ ∏𝑖 ∈ 𝐴𝑛(𝑖), where the sums and products stand in for disjoint union and infinite cartesian product. The version here is proven with unions rather than disjoint unions for convenience, but the version with disjoint unions is clearly a special case of this version. The Axiom of Choice is needed for this proof, but it contains AC as a simple corollary (letting 𝑚(𝑖) = ∅, this theorem says that an infinite cartesian product of nonempty sets is nonempty), so this is an AC equivalent. Theorem 11.26 of [TakeutiZaring] p. 107. (Contributed by Mario Carneiro, 22-Feb-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝑆 = ∪ 𝑖 ∈ 𝐴 (𝑀‘𝑖)    &   ⊢ 𝑃 = X𝑖 ∈ 𝐴 (𝑁‘𝑖)    ⇒   ⊢ (∀𝑖 ∈ 𝐴 (𝑀‘𝑖) ≺ (𝑁‘𝑖) → 𝑆 ≺ 𝑃)
Theorem	alephsucpw 10607	The power set of an aleph dominates the successor aleph. (The Generalized Continuum Hypothesis says they are equinumerous, see gch3 10713 or gchaleph2 10709.) (Contributed by NM, 27-Aug-2005.)
⊢ (ℵ‘suc 𝐴) ≼ 𝒫 (ℵ‘𝐴)
Theorem	aleph1 10608	The set exponentiation of 2 to the aleph-zero has cardinality of at least aleph-one. (If we were to assume the Continuum Hypothesis, their cardinalities would be the same.) (Contributed by NM, 7-Jul-2004.)
⊢ (ℵ‘1o) ≼ (2o ↑m (ℵ‘∅))
Theorem	alephval2 10609*	An alternate way to express the value of the aleph function for nonzero arguments. Theorem 64 of [Suppes] p. 229. (Contributed by NM, 15-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (ℵ‘𝐴) = ∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑥})
Theorem	dominfac 10610	A nonempty set that is a subset of its union is infinite. This version is proved from ax-ac 10496. See dominf 10482 for a version proved from ax-cc 10472. (Contributed by NM, 25-Mar-2007.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ ∪ 𝐴) → ω ≼ 𝐴)
3.2.4  Cardinal number arithmetic using Axiom of Choice
Theorem	iunctb 10611*	The countable union of countable sets is countable (indexed union version of unictb 10612). (Contributed by Mario Carneiro, 18-Jan-2014.)
⊢ ((𝐴 ≼ ω ∧ ∀𝑥 ∈ 𝐴 𝐵 ≼ ω) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ω)
Theorem	unictb 10612*	The countable union of countable sets is countable. Theorem 6Q of [Enderton] p. 159. See iunctb 10611 for indexed union version. (Contributed by NM, 26-Mar-2006.)
⊢ ((𝐴 ≼ ω ∧ ∀𝑥 ∈ 𝐴 𝑥 ≼ ω) → ∪ 𝐴 ≼ ω)
Theorem	infmap 10613*	An exponentiation law for infinite cardinals. Similar to Lemma 6.2 of [Jech] p. 43. (Contributed by NM, 1-Oct-2004.) (Proof shortened by Mario Carneiro, 30-Apr-2015.)
⊢ ((ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴) → (𝐴 ↑m 𝐵) ≈ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐵)})
Theorem	alephadd 10614	The sum of two alephs is their maximum. Equation 6.1 of [Jech] p. 42. (Contributed by NM, 29-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ≈ ((ℵ‘𝐴) ∪ (ℵ‘𝐵))
Theorem	alephmul 10615	The product of two alephs is their maximum. Equation 6.1 of [Jech] p. 42. (Contributed by NM, 29-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((ℵ‘𝐴) × (ℵ‘𝐵)) ≈ ((ℵ‘𝐴) ∪ (ℵ‘𝐵)))
Theorem	alephexp1 10616	An exponentiation law for alephs. Lemma 6.1 of [Jech] p. 42. (Contributed by NM, 29-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐴 ⊆ 𝐵) → ((ℵ‘𝐴) ↑m (ℵ‘𝐵)) ≈ (2o ↑m (ℵ‘𝐵)))
Theorem	alephsuc3 10617*	An alternate representation of a successor aleph. Compare alephsuc 10105 and alephsuc2 10117. Equality can be obtained by taking the card of the right-hand side then using alephcard 10107 and carden 10588. (Contributed by NM, 23-Oct-2004.)
⊢ (𝐴 ∈ On → (ℵ‘suc 𝐴) ≈ {𝑥 ∈ On ∣ 𝑥 ≈ (ℵ‘𝐴)})
Theorem	alephexp2 10618*	An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 10616 (which works if the base is less than or equal to the exponent) and infmap 10613 (which works if the exponent is less than or equal to the base). They can be equated only when the base is equal to the exponent, and this is the result. (Contributed by NM, 23-Oct-2004.)
⊢ (𝐴 ∈ On → (2o ↑m (ℵ‘𝐴)) ≈ {𝑥 ∣ (𝑥 ⊆ (ℵ‘𝐴) ∧ 𝑥 ≈ (ℵ‘𝐴))})
3.2.5  Cofinality using the Axiom of Choice
Theorem	alephreg 10619	A successor aleph is regular. Theorem 11.15 of [TakeutiZaring] p. 103. (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ (cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴)
Theorem	pwcfsdom 10620*	A corollary of Konig's Theorem konigth 10606. Theorem 11.28 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ 𝐻 = (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑦)))    ⇒   ⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴)))
Theorem	cfpwsdom 10621	A corollary of Konig's Theorem konigth 10606. Theorem 11.29 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴)))))
Theorem	alephom 10622	From canth2 9168, we know that (ℵ‘0) < (2↑ω), but we cannot prove that (2↑ω) = (ℵ‘1) (this is the Continuum Hypothesis), nor can we prove that it is less than any bound whatsoever (i.e. the statement (ℵ‘𝐴) < (2↑ω) is consistent for any ordinal 𝐴). However, we can prove that (2↑ω) is not equal to (ℵ‘ω), nor (ℵ‘(ℵ‘ω)), on cofinality grounds, because by Konig's Theorem konigth 10606 (in the form of cfpwsdom 10621), (2↑ω) has uncountable cofinality, which eliminates limit alephs like (ℵ‘ω). (The first limit aleph that is not eliminated is (ℵ‘(ℵ‘1)), which has cofinality (ℵ‘1).) (Contributed by Mario Carneiro, 21-Mar-2013.)
⊢ (card‘(2o ↑m ω)) ≠ (ℵ‘ω)
Theorem	smobeth 10623	The beth function is strictly monotone. This function is not strictly the beth function, but rather bethA is the same as (card‘(𝑅1‘(ω +o 𝐴))), since conventionally we start counting at the first infinite level, and ignore the finite levels. (Contributed by Mario Carneiro, 6-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2015.)
⊢ Smo (card ∘ 𝑅1)
3.3  ZFC Axioms with no distinct variable requirements
Theorem	nd1 10624	A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑦 ∈ 𝑧)
Theorem	nd2 10625	A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑧 ∈ 𝑦)
Theorem	nd3 10626	A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002.)
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑧 𝑥 ∈ 𝑦)
Theorem	nd4 10627	A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑧 𝑦 ∈ 𝑥)
Theorem	axextnd 10628	A version of the Axiom of Extensionality with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 14-Aug-2003.) (New usage is discouraged.)
⊢ ∃𝑥((𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)
Theorem	axrepndlem1 10629*	Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
Theorem	axrepndlem2 10630	Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (New usage is discouraged.)
⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))))
Theorem	axrepnd 10631	A version of the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(∀𝑦 𝑧 ∈ 𝑥 ↔ ∃𝑥(∀𝑧 𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
Theorem	axunndlem1 10632*	Lemma for the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axunnd 10633	A version of the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpowndlem1 10634	Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.)
⊢ (∀𝑥 𝑥 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))
Theorem	axpowndlem2 10635*	Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (Revised and shortened by Wolf Lammen, 9-Jun-2019.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))
Theorem	axpowndlem3 10636*	Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 4-Jan-2002.) (Revised by Mario Carneiro, 10-Dec-2016.) (Proof shortened by Wolf Lammen, 10-Jun-2019.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))
Theorem	axpowndlem4 10637	Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) (New usage is discouraged.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))))
Theorem	axpownd 10638	A version of the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 4-Jan-2002.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))
Theorem	axregndlem1 10639	Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))))
Theorem	axregndlem2 10640*	Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	axregnd 10641	A version of the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Wolf Lammen, 18-Aug-2019.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	axinfndlem1 10642*	Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.)
⊢ (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))
Theorem	axinfnd 10643	A version of the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.)
⊢ ∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))
Theorem	axacndlem1 10644	Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
Theorem	axacndlem2 10645	Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
Theorem	axacndlem3 10646	Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.)
⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
Theorem	axacndlem4 10647*	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 10648*	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 10649	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 10650*	Axiom of Extensionality ax-ext 2705, reproved from conditionless ZFC version and predicate calculus. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	zfcndrep 10651*	Axiom of Replacement ax-rep 5284, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	zfcndun 10652*	Axiom of Union ax-un 7753, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfcndpow 10653*	Axiom of Power Sets ax-pow 5370, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru 5446. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	zfcndreg 10654*	Axiom of Regularity ax-reg 9629, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2374. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	zfcndinf 10655*	Axiom of Infinity ax-inf 9675, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5447 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦)))
Theorem	zfcndac 10656*	Axiom of Choice ax-ac 10496, 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 10657	Extend class notation to include the collection of sets that satisfy the GCH.
class GCH
Definition	df-gch 10658*	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 10659*	Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴))))
Theorem	fingch 10660	A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ Fin ⊆ GCH
Theorem	gchi 10661	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 10662	If 𝐴 ≤ 𝐵 < 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐴 = 𝐵 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴)) → 𝐴 ≈ 𝐵)
Theorem	gchen2 10663	If 𝐴 < 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → 𝐵 ≈ 𝒫 𝐴)
Theorem	gchor 10664	If 𝐴 ≤ 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then either 𝐴 = 𝐵 or 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → (𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴))
Theorem	engch 10665	The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ GCH ↔ 𝐵 ∈ GCH))
Theorem	gchdomtri 10666	Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 10718. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴))
Theorem	fpwwe2cbv 10667*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 3-Jun-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    ⇒   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))}
Theorem	fpwwe2lem1 10668*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    ⇒   ⊢ 𝑊 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴))
Theorem	fpwwe2lem2 10669*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
Theorem	fpwwe2lem3 10670*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → ((◡𝑅 “ {𝐵})𝐹(𝑅 ∩ ((◡𝑅 “ {𝐵}) × (◡𝑅 “ {𝐵})))) = 𝐵)
Theorem	fpwwe2lem4 10671*	Lemma for fpwwe2 10680. (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 10672*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑁)    &   ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶)))
Theorem	fpwwe2lem6 10673*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ (𝜑 → 𝑋𝑊𝑅)    &   ⊢ (𝜑 → 𝑌𝑊𝑆)    &   ⊢ 𝑀 = OrdIso(𝑅, 𝑋)    &   ⊢ 𝑁 = OrdIso(𝑆, 𝑌)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐵 ∈ dom 𝑁)    &   ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))    ⇒   ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷))))
Theorem	fpwwe2lem7 10674*	Lemma for fpwwe2 10680. 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 10675*	Lemma for fpwwe2 10680. 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 10676*	Lemma for fpwwe2 10680. 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 10677*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋))
Theorem	fpwwe2lem11 10678*	Lemma for fpwwe2 10680. (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 10679*	Lemma for fpwwe2 10680. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ dom 𝑊    ⇒   ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋)
Theorem	fpwwe2 10680*	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 10067. 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 10681*	Lemma for fpwwe 10683. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    ⇒   ⊢ 𝑊 = {⟨𝑎, 𝑠⟩ ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))}
Theorem	fpwwelem 10682*	Lemma for fpwwe 10683. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝐹‘(◡𝑅 “ {𝑦})) = 𝑦))))
Theorem	fpwwe 10683*	Given any function 𝐹 from the powerset of 𝐴 to 𝐴, canth2 9168 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 10067. 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 10684*	An "effective" form of Cantor's theorem canth 7384. 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 10685*	Lemma for canthnum 10686. (Contributed by Mario Carneiro, 19-May-2015.)
⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    &   ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})    ⇒   ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴)
Theorem	canthnum 10686	The set of well-orderable subsets of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 9168. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ (𝒫 𝐴 ∩ dom card))
Theorem	canthwelem 10687*	Lemma for canthwe 10688. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}    &   ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    &   ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})    ⇒   ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:𝑂–1-1→𝐴)
Theorem	canthwe 10688*	The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 9168. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ 𝑂 = {⟨𝑥, 𝑟⟩ ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂)
Theorem	canthp1lem1 10689	Lemma for canthp1 10691. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
Theorem	canthp1lem2 10690*	Lemma for canthp1 10691. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝜑 → 1o ≺ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o))    &   ⊢ (𝜑 → 𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴)    &   ⊢ 𝐻 = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))    &   ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐻‘(◡𝑟 “ {𝑦})) = 𝑦))}    &   ⊢ 𝐵 = ∪ dom 𝑊    ⇒   ⊢ ¬ 𝜑
Theorem	canthp1 10691	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 10692	The exclusion of finite sets from consideration in df-gch 10658 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 10693	An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 1o) ≈ 𝐴)
Theorem	gchinf 10694	An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.)
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝐴)
Theorem	pwfseqlem1 10695*	Lemma for pwfseq 10701. 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 10696*	Lemma for pwfseq 10701. (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 10697*	Lemma for pwfseq 10701. Using the construction 𝐷 from pwfseqlem1 10695, 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 10698*	Lemma for pwfseqlem4 10699. (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 10699*	Lemma for pwfseq 10701. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10697. Applying fpwwe2 10680 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 10700*	Lemma for pwfseq 10701. Although in some ways pwfseqlem4 10699 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 10064. 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 10051. 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 9743), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10055). (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 𝑦)‘𝑦)⟩)    &   ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ ⟨(𝑂‘𝑥), 𝑦⟩)    &   ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄)    ⇒   ⊢ ¬ 𝜑