P. 95 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	alephexp1 9401	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.)
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( ( aleph ` A ) ^m ( aleph ` B ) ) ~~ ( 2o ^m ( aleph ` B ) ) )
Theorem	alephsuc3 9402*	An alternate representation of a successor aleph. Compare alephsuc 8891 and alephsuc2 8903. Equality can be obtained by taking the card of the right-hand side then using alephcard 8893 and carden 9373. (Contributed by NM, 23-Oct-2004.)
|- ( A e. On -> ( aleph ` suc A ) ~~ { x e. On | x ~~ ( aleph ` A ) } )
Theorem	alephexp2 9403*	An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 9401 (which works if the base is less than or equal to the exponent) and infmap 9398 (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.)
|- ( A e. On -> ( 2o ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } )
3.2.5  Cofinality using Axiom of Choice
Theorem	alephreg 9404	A successor aleph is regular. Theorem 11.15 of [TakeutiZaring] p. 103. (Contributed by Mario Carneiro, 9-Mar-2013.)
|- ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A )
Theorem	pwcfsdom 9405*	A corollary of Konig's Theorem konigth 9391. Theorem 11.28 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.)
|- H = ( y e. ( cf ` ( aleph ` A ) ) |-> (har ` ( f ` y ) ) )   =>    |- ( aleph ` A ) ~< ( ( aleph ` A ) ^m ( cf ` ( aleph ` A ) ) )
Theorem	cfpwsdom 9406	A corollary of Konig's Theorem konigth 9391. Theorem 11.29 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.)
|- B e. _V   =>    |- ( 2o ~<_ B -> ( aleph ` A ) ~< ( cf ` ( card ` ( B ^m ( aleph ` A ) ) ) ) )
Theorem	alephom 9407	From canth2 8113, we know that ( aleph ` 0 ) < ( 2 ^ om ), but we cannot prove that ( 2 ^ om ) = ( aleph ` 1 ) (this is the Continuum Hypothesis), nor can we prove that it is less than any bound whatsoever (i.e. the statement ( aleph ` A ) < ( 2 ^ om ) is consistent for any ordinal A). However, we can prove that ( 2 ^ om ) is not equal to ( aleph ` om ), nor ( aleph ` ( aleph ` om ) ), on cofinality grounds, because by Konig's Theorem konigth 9391 (in the form of cfpwsdom 9406), ( 2 ^ om ) has uncountable cofinality, which eliminates limit alephs like ( aleph ` om ). (The first limit aleph that is not eliminated is ( aleph ` ( aleph ` 1 ) ), which has cofinality ( aleph ` 1 ).) (Contributed by Mario Carneiro, 21-Mar-2013.)
|- ( card ` ( 2o ^m om ) ) =/= ( aleph ` om )
Theorem	smobeth 9408	The beth function is strictly monotone. This function is not strictly the beth function, but rather bethA is the same as ( card ` ( R1 ` ( om +o A ) ) ), 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 o. R1 )
3.3  ZFC Axioms with no distinct variable requirements
Theorem	nd1 9409	A lemma for proving conditionless ZFC axioms. (Contributed by NM, 1-Jan-2002.)
|- ( A. x x = y -> -. A. x y e. z )
Theorem	nd2 9410	A lemma for proving conditionless ZFC axioms. (Contributed by NM, 1-Jan-2002.)
|- ( A. x x = y -> -. A. x z e. y )
Theorem	nd3 9411	A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002.)
|- ( A. x x = y -> -. A. z x e. y )
Theorem	nd4 9412	A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002.)
|- ( A. x x = y -> -. A. z y e. x )
Theorem	axextnd 9413	A version of the Axiom of Extensionality with no distinct variable conditions. (Contributed by NM, 14-Aug-2003.)
|- E. x ( ( x e. y <-> x e. z ) -> y = z )
Theorem	axrepndlem1 9414*	Lemma for the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.)
|- ( -. A. y y = z -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
Theorem	axrepndlem2 9415	Lemma for the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
|- ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ -. A. y y = z ) -> E. x ( E. y A. z ( ph -> z = y ) -> A. z ( z e. x <-> E. x ( x e. y /\ A. y ph ) ) ) )
Theorem	axrepnd 9416	A version of the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.)
|- E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
Theorem	axunndlem1 9417*	Lemma for the Axiom of Union with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.)
|- E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )
Theorem	axunnd 9418	A version of the Axiom of Union with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.)
|- E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )
Theorem	axpowndlem1 9419	Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.)
|- ( A. x x = y -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
Theorem	axpowndlem2 9420*	Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (Revised and shortened by Wolf Lammen, 9-Jun-2019.)
|- ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
Theorem	axpowndlem3 9421*	Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) (Revised by Mario Carneiro, 10-Dec-2016.) (Proof shortened by Wolf Lammen, 10-Jun-2019.)
|- ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
Theorem	axpowndlem4 9422	Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)
|- ( -. A. y y = x -> ( -. A. y y = z -> ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
Theorem	axpownd 9423	A version of the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.)
|- ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
Theorem	axregndlem1 9424	Lemma for the Axiom of Regularity with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.)
|- ( A. x x = z -> ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) ) )
Theorem	axregndlem2 9425*	Lemma for the Axiom of Regularity with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)
|- ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )
Theorem	axregnd 9426	A version of the Axiom of Regularity with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Wolf Lammen, 18-Aug-2019.)
|- ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )
Theorem	axinfndlem1 9427*	Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.)
|- ( A. x y e. z -> E. x ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
Theorem	axinfnd 9428	A version of the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.)
|- E. x ( y e. z -> ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
Theorem	axacndlem1 9429	Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.)
|- ( A. x x = y -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
Theorem	axacndlem2 9430	Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.)
|- ( A. x x = z -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
Theorem	axacndlem3 9431	Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.)
|- ( A. y y = z -> E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) ) )
Theorem	axacndlem4 9432*	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.)
|- E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
Theorem	axacndlem5 9433*	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.)
|- E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
Theorem	axacnd 9434	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.)
|- E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )
Theorem	zfcndext 9435*	Axiom of Extensionality ax-ext 2602, reproved from conditionless ZFC version and predicate calculus. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.)
|- ( A. z ( z e. x <-> z e. y ) -> x = y )
Theorem	zfcndrep 9436*	Axiom of Replacement ax-rep 4771, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.)
|- ( A. w E. y A. z ( A. y ph -> z = y ) -> E. y A. z ( z e. y <-> E. w ( w e. x /\ A. y ph ) ) )
Theorem	zfcndun 9437*	Axiom of Union ax-un 6949, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.)
|- E. y A. z ( E. w ( z e. w /\ w e. x ) -> z e. y )
Theorem	zfcndpow 9438*	Axiom of Power Sets ax-pow 4843, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness," dtru 4857. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.)
|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
Theorem	zfcndreg 9439*	Axiom of Regularity ax-reg 8497, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.)
|- ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )
Theorem	zfcndinf 9440*	Axiom of Infinity ax-inf 8535, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing theorem el 4847 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.)
|- E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) )
Theorem	zfcndac 9441*	Axiom of Choice ax-ac 9281, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (New usage is discouraged.) (Proof modification is discouraged.)
|- E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) )
3.4  The Generalized Continuum Hypothesis
3.4.1  Sets satisfying the Generalized Continuum Hypothesis
Syntax	cgch 9442	Extend class notation to include the collection of sets that satisfy the GCH.
class GCH
Definition	df-gch 9443*	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 x satisfies the generalized continuum hypothesis if it is finite or there is no set y strictly between x and its powerset in cardinality. The continuum hypothesis is equivalent to om e. GCH. (Contributed by Mario Carneiro, 15-May-2015.)
|- GCH = ( Fin u. { x | A. y -. ( x ~< y /\ y ~< ~P x ) } )
Theorem	elgch 9444*	Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( A e. V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )
Theorem	fingch 9445	A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.)
|- Fin C_ GCH
Theorem	gchi 9446	The only GCH-sets which have other sets between it and its power set are finite sets. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( A e. GCH /\ A ~< B /\ B ~< ~P A ) -> A e. Fin )
Theorem	gchen1 9447	If A <_ B < ~P A, and A is an infinite GCH-set, then A = B in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ B /\ B ~< ~P A ) ) -> A ~~ B )
Theorem	gchen2 9448	If A < B <_ ~P A, and A is an infinite GCH-set, then B = ~P A in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~< B /\ B ~<_ ~P A ) ) -> B ~~ ~P A )
Theorem	gchor 9449	If A <_ B <_ ~P A, and A is an infinite GCH-set, then either A = B or B = ~P A in cardinality. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~<_ B /\ B ~<_ ~P A ) ) -> ( A ~~ B \/ B ~~ ~P A ) )
Theorem	engch 9450	The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( A ~~ B -> ( A e. GCH <-> B e. GCH ) )
Theorem	gchdomtri 9451	Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 9503. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( A e. GCH /\ ( A +c A ) ~~ A /\ B ~<_ ~P A ) -> ( A ~<_ B \/ B ~<_ A ) )
Theorem	fpwwe2cbv 9452*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 3-Jun-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   =>    |- W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = z ) ) }
Theorem	fpwwe2lem1 9453*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   =>    |- W C_ ( ~P A X. ~P ( A X. A ) )
Theorem	fpwwe2lem2 9454*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 19-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   =>    |- ( ph -> ( X W R <-> ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) )
Theorem	fpwwe2lem3 9455*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 19-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ph -> X W R )   =>    |- ( ( ph /\ B e. X ) -> ( ( `' R " { B } ) F ( R i^i ( ( `' R " { B } ) X. ( `' R " { B } ) ) ) ) = B )
Theorem	fpwwe2lem5 9456*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   =>    |- ( ( ph /\ ( X C_ A /\ R C_ ( X X. X ) /\ R We X ) ) -> ( X F R ) e. A )
Theorem	fpwwe2lem6 9457*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- ( ph -> X W R )   &    |- ( ph -> Y W S )   &    |- M = OrdIso ( R , X )   &    |- N = OrdIso ( S , Y )   &    |- ( ph -> B e. dom M )   &    |- ( ph -> B e. dom N )   &    |- ( ph -> ( M |` B ) = ( N |` B ) )   =>    |- ( ( ph /\ C R ( M ` B ) ) -> ( C e. X /\ C e. Y /\ ( `' M ` C ) = ( `' N ` C ) ) )
Theorem	fpwwe2lem7 9458*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- ( ph -> X W R )   &    |- ( ph -> Y W S )   &    |- M = OrdIso ( R , X )   &    |- N = OrdIso ( S , Y )   &    |- ( ph -> B e. dom M )   &    |- ( ph -> B e. dom N )   &    |- ( ph -> ( M |` B ) = ( N |` B ) )   =>    |- ( ( ph /\ C R ( M ` B ) ) -> ( C S ( N ` B ) /\ ( D R ( M ` B ) -> ( C R D <-> C S D ) ) ) )
Theorem	fpwwe2lem8 9459*	Lemma for fpwwe2 9465. Show by induction that the two isometries M and N agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- ( ph -> X W R )   &    |- ( ph -> Y W S )   &    |- M = OrdIso ( R , X )   &    |- N = OrdIso ( S , Y )   &    |- ( ph -> dom M C_ dom N )   =>    |- ( ph -> M = ( N |` dom M ) )
Theorem	fpwwe2lem9 9460*	Lemma for fpwwe2 9465. Given two well-orders <. X , R >. and <. Y , S >. of parts of A, one is an initial segment of the other. (The O C_ P hypothesis is in order to break the symmetry of X and Y.) (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- ( ph -> X W R )   &    |- ( ph -> Y W S )   &    |- M = OrdIso ( R , X )   &    |- N = OrdIso ( S , Y )   &    |- ( ph -> dom M C_ dom N )   =>    |- ( ph -> ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) )
Theorem	fpwwe2lem10 9461*	Lemma for fpwwe2 9465. Given two well-orders <. X , R >. and <. Y , S >. of parts of A, one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- ( ph -> X W R )   &    |- ( ph -> Y W S )   =>    |- ( ph -> ( ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) \/ ( Y C_ X /\ S = ( R i^i ( X X. Y ) ) ) ) )
Theorem	fpwwe2lem11 9462*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- X = U. dom W   =>    |- ( ph -> W : dom W --> ~P ( X X. X ) )
Theorem	fpwwe2lem12 9463*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- X = U. dom W   =>    |- ( ph -> X e. dom W )
Theorem	fpwwe2lem13 9464*	Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- X = U. dom W   =>    |- ( ph -> ( X F ( W ` X ) ) e. X )
Theorem	fpwwe2 9465*	Given any function F from well-orderings of subsets of A to A, there is a unique well-ordered subset <. X , ( W ` X ) >. which "agrees" with F 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 8853. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )   &    |- X = U. dom W   =>    |- ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )
Theorem	fpwwecbv 9466*	Lemma for fpwwe 9468. (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }   =>    |- W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( F ` ( `' s " { z } ) ) = z ) ) }
Theorem	fpwwelem 9467*	Lemma for fpwwe 9468. (Contributed by Mario Carneiro, 15-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }   &    |- ( ph -> A e. _V )   =>    |- ( ph -> ( X W R <-> ( ( X C_ A /\ R C_ ( X X. X ) ) /\ ( R We X /\ A. y e. X ( F ` ( `' R " { y } ) ) = y ) ) ) )
Theorem	fpwwe 9468*	Given any function F from the powerset of A to A, canth2 8113 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset <. X , ( W ` X ) >. which "agrees" with F 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 8853. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }   &    |- ( ph -> A e. _V )   &    |- ( ( ph /\ x e. ( ~P A i^i dom card ) ) -> ( F ` x ) e. A )   &    |- X = U. dom W   =>    |- ( ph -> ( ( Y W R /\ ( F ` Y ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )
Theorem	canth4 9469*	An "effective" form of Cantor's theorem canth 6608. For any function F from the powerset of A to A, there are two definable sets B and C which witness non-injectivity of F. Corollary 1.3 of [KanamoriPincus] p. 416. (Contributed by Mario Carneiro, 18-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }   &    |- B = U. dom W   &    |- C = ( `' ( W ` B ) " { ( F ` B ) } )   =>    |- ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )
Theorem	canthnumlem 9470*	Lemma for canthnum 9471. (Contributed by Mario Carneiro, 19-May-2015.)
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }   &    |- B = U. dom W   &    |- C = ( `' ( W ` B ) " { ( F ` B ) } )   =>    |- ( A e. V -> -. F : ( ~P A i^i dom card ) -1-1-> A )
Theorem	canthnum 9471	The set of well-orderable subsets of a set A strictly dominates A. A stronger form of canth2 8113. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.)
|- ( A e. V -> A ~< ( ~P A i^i dom card ) )
Theorem	canthwelem 9472*	Lemma for canthwe 9473. (Contributed by Mario Carneiro, 31-May-2015.)
|- O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }   &    |- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }   &    |- B = U. dom W   &    |- C = ( `' ( W ` B ) " { ( B F ( W ` B ) ) } )   =>    |- ( A e. V -> -. F : O -1-1-> A )
Theorem	canthwe 9473*	The set of well-orders of a set A strictly dominates A. A stronger form of canth2 8113. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.)
|- O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }   =>    |- ( A e. V -> A ~< O )
Theorem	canthp1lem1 9474	Lemma for canthp1 9476. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( 1o ~< A -> ( A +c 2o ) ~<_ ~P A )
Theorem	canthp1lem2 9475*	Lemma for canthp1 9476. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( ph -> 1o ~< A )   &    |- ( ph -> F : ~P A -1-1-onto-> ( A +c 1o ) )   &    |- ( ph -> G : ( ( A +c 1o ) \ { ( F ` A ) } ) -1-1-onto-> A )   &    |- H = ( ( G o. F ) o. ( x e. ~P A |-> if ( x = A , (/) , x ) ) )   &    |- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( H ` ( `' r " { y } ) ) = y ) ) }   &    |- B = U. dom W   =>    |- -. ph
Theorem	canthp1 9476	A slightly stronger form of Cantor's theorem: For 1 < n, n + 1 < 2 ^ n. Corollary 1.6 of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( 1o ~< A -> ( A +c 1o ) ~< ~P A )
Theorem	finngch 9477	The exclusion of finite sets from consideration in df-gch 9443 is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015.)
|- ( ( A e. Fin /\ 1o ~< A ) -> ( A ~< ( A +c 1o ) /\ ( A +c 1o ) ~< ~P A ) )
Theorem	gchcda1 9478	An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.)
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A +c 1o ) ~~ A )
Theorem	gchinf 9479	An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.)
|- ( ( A e. GCH /\ -. A e. Fin ) -> om ~<_ A )
Theorem	pwfseqlem1 9480*	Lemma for pwfseq 9486. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.)
|- ( ph -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )   &    |- ( ph -> X C_ A )   &    |- ( ph -> H : om -1-1-onto-> X )   &    |- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ om ~<_ x ) )   &    |- ( ( ph /\ ps ) -> K : U_ n e. om ( x ^m n ) -1-1-> x )   &    |- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )   =>    |- ( ( ph /\ ps ) -> D e. ( U_ n e. om ( A ^m n ) \ U_ n e. om ( x ^m n ) ) )
Theorem	pwfseqlem2 9481*	Lemma for pwfseq 9486. (Contributed by Mario Carneiro, 18-Nov-2014.) (Revised by AV, 18-Sep-2021.)
|- ( ph -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )   &    |- ( ph -> X C_ A )   &    |- ( ph -> H : om -1-1-onto-> X )   &    |- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ om ~<_ x ) )   &    |- ( ( ph /\ ps ) -> K : U_ n e. om ( x ^m n ) -1-1-> x )   &    |- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )   &    |- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) )   =>    |- ( ( Y e. Fin /\ R e. V ) -> ( Y F R ) = ( H ` ( card ` Y ) ) )
Theorem	pwfseqlem3 9482*	Lemma for pwfseq 9486. Using the construction D from pwfseqlem1 9480, produce a function F that maps any well-ordered infinite set to an element outside the set. (Contributed by Mario Carneiro, 31-May-2015.)
|- ( ph -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )   &    |- ( ph -> X C_ A )   &    |- ( ph -> H : om -1-1-onto-> X )   &    |- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ om ~<_ x ) )   &    |- ( ( ph /\ ps ) -> K : U_ n e. om ( x ^m n ) -1-1-> x )   &    |- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )   &    |- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) )   =>    |- ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) )
Theorem	pwfseqlem4a 9483*	Lemma for pwfseqlem4 9484. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- ( ph -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )   &    |- ( ph -> X C_ A )   &    |- ( ph -> H : om -1-1-onto-> X )   &    |- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ om ~<_ x ) )   &    |- ( ( ph /\ ps ) -> K : U_ n e. om ( x ^m n ) -1-1-> x )   &    |- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )   &    |- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) )   =>    |- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a F s ) e. A )
Theorem	pwfseqlem4 9484*	Lemma for pwfseq 9486. Derive a final contradiction from the function F in pwfseqlem3 9482. Applying fpwwe2 9465 to it, we get a certain maximal well-ordered subset Z, but the defining property ( Z F ( W ` Z ) ) e. Z contradicts our assumption on F, so we are reduced to the case of Z finite. This too is a contradiction, though, because Z and its preimage under ( W ` Z ) 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.)
|- ( ph -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )   &    |- ( ph -> X C_ A )   &    |- ( ph -> H : om -1-1-onto-> X )   &    |- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ om ~<_ x ) )   &    |- ( ( ph /\ ps ) -> K : U_ n e. om ( x ^m n ) -1-1-> x )   &    |- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )   &    |- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) )   &    |- W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. b e. a [. ( `' s " { b } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = b ) ) }   &    |- Z = U. dom W   =>    |- -. ph
Theorem	pwfseqlem5 9485*	Lemma for pwfseq 9486. Although in some ways pwfseqlem4 9484 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 K from the set of finite sequences on an infinite set x to x. Now this alone would not be difficult to prove; this is mostly the claim of fseqen 8850. 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 8837. 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 8603), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 8841). (Contributed by Mario Carneiro, 31-May-2015.)
|- ( ph -> G : ~P A -1-1-> U_ n e. om ( A ^m n ) )   &    |- ( ph -> X C_ A )   &    |- ( ph -> H : om -1-1-onto-> X )   &    |- ( ps <-> ( ( t C_ A /\ r C_ ( t X. t ) /\ r We t ) /\ om ~<_ t ) )   &    |- ( ph -> A. b e. (har ` ~P A ) ( om C_ b -> ( N ` b ) : ( b X. b ) -1-1-onto-> b ) )   &    |- O = OrdIso ( r , t )   &    |- T = ( u e. dom O , v e. dom O |-> <. ( O ` u ) , ( O ` v ) >. )   &    |- P = ( ( O o. ( N ` dom O ) ) o. `' T )   &    |- S = seq𝜔 ( ( k e. _V , f e. _V |-> ( x e. ( t ^m suc k ) |-> ( ( f ` ( x |` k ) ) P ( x ` k ) ) ) ) , { <. (/) , ( O ` (/) ) >. } )   &    |- Q = ( y e. U_ n e. om ( t ^m n ) |-> <. dom y , ( ( S ` dom y ) ` y ) >. )   &    |- I = ( x e. om , y e. t |-> <. ( O ` x ) , y >. )   &    |- K = ( ( P o. I ) o. Q )   =>    |- -. ph
Theorem	pwfseq 9486*	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.)
|- ( om ~<_ A -> -. ~P A ~<_ U_ n e. om ( A ^m n ) )
Theorem	pwxpndom2 9487	The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.)
|- ( om ~<_ A -> -. ~P A ~<_ ( A +c ( A X. A ) ) )
Theorem	pwxpndom 9488	The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.)
|- ( om ~<_ A -> -. ~P A ~<_ ( A X. A ) )
Theorem	pwcdandom 9489	The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015.)
|- ( om ~<_ A -> -. ~P A ~<_ ( A +c A ) )
Theorem	gchcdaidm 9490	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.)
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A +c A ) ~~ A )
Theorem	gchxpidm 9491	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.)
|- ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~~ A )
Theorem	gchpwdom 9492	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.)
|- ( ( om ~<_ A /\ A e. GCH /\ B e. GCH ) -> ( A ~< B <-> ~P A ~<_ B ) )
Theorem	gchaleph 9493	If ( aleph ` A ) is a GCH-set and its powerset is well-orderable, then the successor aleph ( aleph ` suc A ) is equinumerous to the powerset of ( aleph ` A ). (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ~P ( aleph ` A ) e. dom card ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) )
Theorem	gchaleph2 9494	If ( aleph ` A ) and ( aleph ` suc A ) are GCH-sets, then the successor aleph ( aleph ` suc A ) is equinumerous to the powerset of ( aleph ` A ). (Contributed by Mario Carneiro, 31-May-2015.)
|- ( ( A e. On /\ ( aleph ` A ) e. GCH /\ ( aleph ` suc A ) e. GCH ) -> ( aleph ` suc A ) ~~ ~P ( aleph ` A ) )
Theorem	hargch 9495	If A + ~~ ~P A, then A is a GCH-set. The much simpler converse to gchhar 9501. (Contributed by Mario Carneiro, 2-Jun-2015.)
|- ( (har ` A ) ~~ ~P A -> A e. GCH )
Theorem	alephgch 9496	If ( aleph ` suc A ) is equinumerous to the powerset of ( aleph ` A ), then ( aleph ` A ) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( aleph ` suc A ) ~~ ~P ( aleph ` A ) -> ( aleph ` A ) e. GCH )
Theorem	gch2 9497	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 aleph C_ GCH )
Theorem	gch3 9498	An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.)
|- (GCH = _V <-> A. x e. On ( aleph ` suc x ) ~~ ~P ( aleph ` x ) )
Theorem	gch-kn 9499*	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 9403 to the successor aleph using enen2 8101. (Contributed by NM, 1-Oct-2004.)
|- ( A e. On -> ( ( aleph ` suc A ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } <-> ( aleph ` suc A ) ~~ ( 2o ^m ( aleph ` A ) ) ) )
3.4.2  Derivation of the Axiom of Choice
Theorem	gchaclem 9500	Lemma for gchac 9503 (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ph -> om ~<_ A )   &    |- ( ph -> ~P C e. GCH )   &    |- ( ph -> ( A ~<_ C /\ ( B ~<_ ~P C -> ~P A ~<_ B ) ) )   =>    |- ( ph -> ( A ~<_ ~P C /\ ( B ~<_ ~P ~P C -> ~P A ~<_ B ) ) )