Metamath Proof Explorer

Theorem alephexp2

Description: An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 (which works if the base is less than or equal to the exponent) and infmap (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)

Ref Expression
Assertion alephexp2 
|- ( A e. On -> ( 2o ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } )

Proof

Step Hyp Ref Expression
1 alephgeom 
 |-  ( A e. On <-> _om C_ ( aleph ` A ) )
2 fvex 
 |-  ( aleph ` A ) e. _V
3 ssdomg 
 |-  ( ( aleph ` A ) e. _V -> ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) ) )
4 2 3 ax-mp 
 |-  ( _om C_ ( aleph ` A ) -> _om ~<_ ( aleph ` A ) )
5 1 4 sylbi 
 |-  ( A e. On -> _om ~<_ ( aleph ` A ) )
6 domrefg 
 |-  ( ( aleph ` A ) e. _V -> ( aleph ` A ) ~<_ ( aleph ` A ) )
7 2 6 ax-mp 
 |-  ( aleph ` A ) ~<_ ( aleph ` A )
8 infmap 
 |-  ( ( _om ~<_ ( aleph ` A ) /\ ( aleph ` A ) ~<_ ( aleph ` A ) ) -> ( ( aleph ` A ) ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } )
9 5 7 8 sylancl 
 |-  ( A e. On -> ( ( aleph ` A ) ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } )
10 pm3.2 
 |-  ( A e. On -> ( A e. On -> ( A e. On /\ A e. On ) ) )
11 10 pm2.43i 
 |-  ( A e. On -> ( A e. On /\ A e. On ) )
12 ssid 
 |-  A C_ A
13 alephexp1 
 |-  ( ( ( A e. On /\ A e. On ) /\ A C_ A ) -> ( ( aleph ` A ) ^m ( aleph ` A ) ) ~~ ( 2o ^m ( aleph ` A ) ) )
14 11 12 13 sylancl 
 |-  ( A e. On -> ( ( aleph ` A ) ^m ( aleph ` A ) ) ~~ ( 2o ^m ( aleph ` A ) ) )
15 enen1 
 |-  ( ( ( aleph ` A ) ^m ( aleph ` A ) ) ~~ ( 2o ^m ( aleph ` A ) ) -> ( ( ( aleph ` A ) ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } <-> ( 2o ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } ) )
16 14 15 syl 
 |-  ( A e. On -> ( ( ( aleph ` A ) ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } <-> ( 2o ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } ) )
17 9 16 mpbid 
 |-  ( A e. On -> ( 2o ^m ( aleph ` A ) ) ~~ { x | ( x C_ ( aleph ` A ) /\ x ~~ ( aleph ` A ) ) } )