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

Theorem dfac12k 8585
Description: Equivalence of dfac12 8587 and dfac12a 8586, without using Regularity. (Contributed by Mario Carneiro, 21-May-2015.)
Assertion
Ref Expression
dfac12k  |-  ( A. x  e.  On  ~P x  e.  dom  card  <->  A. y  e.  On  ~P ( aleph `  y )  e.  dom  card )
Distinct variable group:    x, y

Proof of Theorem dfac12k
StepHypRef Expression
1 alephon 8508 . . . 4  |-  ( aleph `  y )  e.  On
2 pweq 3984 . . . . . 6  |-  ( x  =  ( aleph `  y
)  ->  ~P x  =  ~P ( aleph `  y
) )
32eleq1d 2491 . . . . 5  |-  ( x  =  ( aleph `  y
)  ->  ( ~P x  e.  dom  card  <->  ~P ( aleph `  y )  e. 
dom  card ) )
43rspcv 3178 . . . 4  |-  ( (
aleph `  y )  e.  On  ->  ( A. x  e.  On  ~P x  e.  dom  card  ->  ~P ( aleph `  y )  e.  dom  card ) )
51, 4ax-mp 5 . . 3  |-  ( A. x  e.  On  ~P x  e.  dom  card  ->  ~P ( aleph `  y )  e.  dom  card )
65ralrimivw 2837 . 2  |-  ( A. x  e.  On  ~P x  e.  dom  card  ->  A. y  e.  On  ~P ( aleph `  y )  e.  dom  card )
7 omelon 8161 . . . . . . 7  |-  om  e.  On
8 cardon 8387 . . . . . . 7  |-  ( card `  x )  e.  On
9 ontri1 5476 . . . . . . 7  |-  ( ( om  e.  On  /\  ( card `  x )  e.  On )  ->  ( om  C_  ( card `  x
)  <->  -.  ( card `  x )  e.  om ) )
107, 8, 9mp2an 676 . . . . . 6  |-  ( om  C_  ( card `  x
)  <->  -.  ( card `  x )  e.  om )
11 cardidm 8402 . . . . . . . 8  |-  ( card `  ( card `  x
) )  =  (
card `  x )
12 cardalephex 8529 . . . . . . . 8  |-  ( om  C_  ( card `  x
)  ->  ( ( card `  ( card `  x
) )  =  (
card `  x )  <->  E. y  e.  On  ( card `  x )  =  ( aleph `  y )
) )
1311, 12mpbii 214 . . . . . . 7  |-  ( om  C_  ( card `  x
)  ->  E. y  e.  On  ( card `  x
)  =  ( aleph `  y ) )
14 r19.29 2960 . . . . . . . . 9  |-  ( ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  /\  E. y  e.  On  ( card `  x
)  =  ( aleph `  y ) )  ->  E. y  e.  On  ( ~P ( aleph `  y
)  e.  dom  card  /\  ( card `  x
)  =  ( aleph `  y ) ) )
15 pweq 3984 . . . . . . . . . . . 12  |-  ( (
card `  x )  =  ( aleph `  y
)  ->  ~P ( card `  x )  =  ~P ( aleph `  y
) )
1615eleq1d 2491 . . . . . . . . . . 11  |-  ( (
card `  x )  =  ( aleph `  y
)  ->  ( ~P ( card `  x )  e.  dom  card  <->  ~P ( aleph `  y
)  e.  dom  card ) )
1716biimparc 489 . . . . . . . . . 10  |-  ( ( ~P ( aleph `  y
)  e.  dom  card  /\  ( card `  x
)  =  ( aleph `  y ) )  ->  ~P ( card `  x
)  e.  dom  card )
1817rexlimivw 2911 . . . . . . . . 9  |-  ( E. y  e.  On  ( ~P ( aleph `  y )  e.  dom  card  /\  ( card `  x )  =  ( aleph `  y )
)  ->  ~P ( card `  x )  e. 
dom  card )
1914, 18syl 17 . . . . . . . 8  |-  ( ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  /\  E. y  e.  On  ( card `  x
)  =  ( aleph `  y ) )  ->  ~P ( card `  x
)  e.  dom  card )
2019ex 435 . . . . . . 7  |-  ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  ->  ( E. y  e.  On  ( card `  x )  =  ( aleph `  y )  ->  ~P ( card `  x
)  e.  dom  card ) )
2113, 20syl5 33 . . . . . 6  |-  ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  ->  ( om  C_  ( card `  x
)  ->  ~P ( card `  x )  e. 
dom  card ) )
2210, 21syl5bir 221 . . . . 5  |-  ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  ->  ( -.  ( card `  x
)  e.  om  ->  ~P ( card `  x
)  e.  dom  card ) )
23 nnfi 7775 . . . . . . 7  |-  ( (
card `  x )  e.  om  ->  ( card `  x )  e.  Fin )
24 pwfi 7879 . . . . . . 7  |-  ( (
card `  x )  e.  Fin  <->  ~P ( card `  x
)  e.  Fin )
2523, 24sylib 199 . . . . . 6  |-  ( (
card `  x )  e.  om  ->  ~P ( card `  x )  e. 
Fin )
26 finnum 8391 . . . . . 6  |-  ( ~P ( card `  x
)  e.  Fin  ->  ~P ( card `  x
)  e.  dom  card )
2725, 26syl 17 . . . . 5  |-  ( (
card `  x )  e.  om  ->  ~P ( card `  x )  e. 
dom  card )
2822, 27pm2.61d2 163 . . . 4  |-  ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  ->  ~P ( card `  x )  e. 
dom  card )
29 oncardid 8399 . . . . 5  |-  ( x  e.  On  ->  ( card `  x )  ~~  x )
30 pwen 7755 . . . . 5  |-  ( (
card `  x )  ~~  x  ->  ~P ( card `  x )  ~~  ~P x )
31 ennum 8390 . . . . 5  |-  ( ~P ( card `  x
)  ~~  ~P x  ->  ( ~P ( card `  x )  e.  dom  card  <->  ~P x  e.  dom  card ) )
3229, 30, 313syl 18 . . . 4  |-  ( x  e.  On  ->  ( ~P ( card `  x
)  e.  dom  card  <->  ~P x  e.  dom  card )
)
3328, 32syl5ibcom 223 . . 3  |-  ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  ->  ( x  e.  On  ->  ~P x  e.  dom  card )
)
3433ralrimiv 2834 . 2  |-  ( A. y  e.  On  ~P ( aleph `  y )  e.  dom  card  ->  A. x  e.  On  ~P x  e. 
dom  card )
356, 34impbii 190 1  |-  ( A. x  e.  On  ~P x  e.  dom  card  <->  A. y  e.  On  ~P ( aleph `  y )  e.  dom  card )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2771   E.wrex 2772    C_ wss 3436   ~Pcpw 3981   class class class wbr 4423   dom cdm 4853   Oncon0 5442   ` cfv 5601   omcom 6707    ~~ cen 7578   Fincfn 7581   cardccrd 8378   alephcale 8379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-inf2 8156
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-2o 7195  df-oadd 7198  df-er 7375  df-map 7486  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-oi 8035  df-har 8083  df-card 8382  df-aleph 8383
This theorem is referenced by:  dfac12  8587
  Copyright terms: Public domain W3C validator