MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alephexp2 Unicode version

Theorem alephexp2 8200
Description: An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 8198 (which works if the base is less than or equal to the exponent) and infmap 8195 (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.)
Assertion
Ref Expression
alephexp2  |-  ( A  e.  On  ->  ( 2o  ^m  ( aleph `  A
) )  ~~  {
x  |  ( x 
C_  ( aleph `  A
)  /\  x  ~~  ( aleph `  A )
) } )
Distinct variable group:    x, A

Proof of Theorem alephexp2
StepHypRef Expression
1 alephgeom 7706 . . . 4  |-  ( A  e.  On  <->  om  C_  ( aleph `  A ) )
2 fvex 5501 . . . . 5  |-  ( aleph `  A )  e.  _V
3 ssdomg 6904 . . . . 5  |-  ( (
aleph `  A )  e. 
_V  ->  ( om  C_  ( aleph `  A )  ->  om 
~<_  ( aleph `  A )
) )
42, 3ax-mp 10 . . . 4  |-  ( om  C_  ( aleph `  A )  ->  om  ~<_  ( aleph `  A
) )
51, 4sylbi 189 . . 3  |-  ( A  e.  On  ->  om  ~<_  ( aleph `  A ) )
6 domrefg 6893 . . . 4  |-  ( (
aleph `  A )  e. 
_V  ->  ( aleph `  A
)  ~<_  ( aleph `  A
) )
72, 6ax-mp 10 . . 3  |-  ( aleph `  A )  ~<_  ( aleph `  A )
8 infmap 8195 . . 3  |-  ( ( om  ~<_  ( aleph `  A
)  /\  ( aleph `  A )  ~<_  ( aleph `  A ) )  -> 
( ( aleph `  A
)  ^m  ( aleph `  A ) )  ~~  { x  |  ( x 
C_  ( aleph `  A
)  /\  x  ~~  ( aleph `  A )
) } )
95, 7, 8sylancl 645 . 2  |-  ( A  e.  On  ->  (
( aleph `  A )  ^m  ( aleph `  A )
)  ~~  { x  |  ( x  C_  ( aleph `  A )  /\  x  ~~  ( aleph `  A ) ) } )
10 pm3.2 436 . . . . 5  |-  ( A  e.  On  ->  ( A  e.  On  ->  ( A  e.  On  /\  A  e.  On )
) )
1110pm2.43i 45 . . . 4  |-  ( A  e.  On  ->  ( A  e.  On  /\  A  e.  On ) )
12 ssid 3200 . . . 4  |-  A  C_  A
13 alephexp1 8198 . . . 4  |-  ( ( ( A  e.  On  /\  A  e.  On )  /\  A  C_  A
)  ->  ( ( aleph `  A )  ^m  ( aleph `  A )
)  ~~  ( 2o  ^m  ( aleph `  A )
) )
1411, 12, 13sylancl 645 . . 3  |-  ( A  e.  On  ->  (
( aleph `  A )  ^m  ( aleph `  A )
)  ~~  ( 2o  ^m  ( aleph `  A )
) )
15 enen1 6998 . . 3  |-  ( ( ( 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
) ) } ) )
1614, 15syl 17 . 2  |-  ( 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 ) ) } ) )
179, 16mpbid 203 1  |-  ( A  e.  On  ->  ( 2o  ^m  ( aleph `  A
) )  ~~  {
x  |  ( x 
C_  ( aleph `  A
)  /\  x  ~~  ( aleph `  A )
) } )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    e. wcel 1687   {cab 2272   _Vcvv 2791    C_ wss 3155   class class class wbr 4026   Oncon0 4393   omcom 4657   ` cfv 5223  (class class class)co 5821   2oc2o 6470    ^m cmap 6769    ~~ cen 6857    ~<_ cdom 6858   alephcale 7566
This theorem is referenced by:  gch-kn  8300
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-rep 4134  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-inf2 7339  ax-ac2 8086
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-ral 2551  df-rex 2552  df-reu 2553  df-rmo 2554  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-pss 3171  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-tp 3651  df-op 3652  df-uni 3831  df-int 3866  df-iun 3910  df-br 4027  df-opab 4081  df-mpt 4082  df-tr 4117  df-eprel 4306  df-id 4310  df-po 4315  df-so 4316  df-fr 4353  df-se 4354  df-we 4355  df-ord 4396  df-on 4397  df-lim 4398  df-suc 4399  df-om 4658  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-isom 5232  df-ov 5824  df-oprab 5825  df-mpt2 5826  df-1st 6085  df-2nd 6086  df-iota 6254  df-riota 6301  df-recs 6385  df-rdg 6420  df-1o 6476  df-2o 6477  df-oadd 6480  df-er 6657  df-map 6771  df-en 6861  df-dom 6862  df-sdom 6863  df-fin 6864  df-oi 7222  df-har 7269  df-card 7569  df-aleph 7570  df-acn 7572  df-ac 7740
  Copyright terms: Public domain W3C validator