Metamath Proof Explorer

Theorem dfac12k

Description: Equivalence of dfac12 and dfac12a , without using Regularity. (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion dfac12k 
|- ( A. x e. On ~P x e. dom card <-> A. y e. On ~P ( aleph ` y ) e. dom card )

Proof

Step Hyp Ref Expression
1 alephon 
 |-  ( aleph ` y ) e. On
2 pweq 
 |-  ( x = ( aleph ` y ) -> ~P x = ~P ( aleph ` y ) )
3 2 eleq1d 
 |-  ( x = ( aleph ` y ) -> ( ~P x e. dom card <-> ~P ( aleph ` y ) e. dom card ) )
4 3 rspcv 
 |-  ( ( aleph ` y ) e. On -> ( A. x e. On ~P x e. dom card -> ~P ( aleph ` y ) e. dom card ) )
5 1 4 ax-mp 
 |-  ( A. x e. On ~P x e. dom card -> ~P ( aleph ` y ) e. dom card )
6 5 ralrimivw 
 |-  ( A. x e. On ~P x e. dom card -> A. y e. On ~P ( aleph ` y ) e. dom card )
7 omelon 
 |-  _om e. On
8 cardon 
 |-  ( card ` x ) e. On
9 ontri1 
 |-  ( ( _om e. On /\ ( card ` x ) e. On ) -> ( _om C_ ( card ` x ) <-> -. ( card ` x ) e. _om ) )
10 7 8 9 mp2an 
 |-  ( _om C_ ( card ` x ) <-> -. ( card ` x ) e. _om )
11 cardidm 
 |-  ( card ` ( card ` x ) ) = ( card ` x )
12 cardalephex 
 |-  ( _om C_ ( card ` x ) -> ( ( card ` ( card ` x ) ) = ( card ` x ) <-> E. y e. On ( card ` x ) = ( aleph ` y ) ) )
13 11 12 mpbii 
 |-  ( _om C_ ( card ` x ) -> E. y e. On ( card ` x ) = ( aleph ` y ) )
14 r19.29 
 |-  ( ( 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 
 |-  ( ( card ` x ) = ( aleph ` y ) -> ~P ( card ` x ) = ~P ( aleph ` y ) )
16 15 eleq1d 
 |-  ( ( card ` x ) = ( aleph ` y ) -> ( ~P ( card ` x ) e. dom card <-> ~P ( aleph ` y ) e. dom card ) )
17 16 biimparc 
 |-  ( ( ~P ( aleph ` y ) e. dom card /\ ( card ` x ) = ( aleph ` y ) ) -> ~P ( card ` x ) e. dom card )
18 17 rexlimivw 
 |-  ( E. y e. On ( ~P ( aleph ` y ) e. dom card /\ ( card ` x ) = ( aleph ` y ) ) -> ~P ( card ` x ) e. dom card )
19 14 18 syl 
 |-  ( ( A. y e. On ~P ( aleph ` y ) e. dom card /\ E. y e. On ( card ` x ) = ( aleph ` y ) ) -> ~P ( card ` x ) e. dom card )
20 19 ex 
 |-  ( A. y e. On ~P ( aleph ` y ) e. dom card -> ( E. y e. On ( card ` x ) = ( aleph ` y ) -> ~P ( card ` x ) e. dom card ) )
21 13 20 syl5 
 |-  ( A. y e. On ~P ( aleph ` y ) e. dom card -> ( _om C_ ( card ` x ) -> ~P ( card ` x ) e. dom card ) )
22 10 21 syl5bir 
 |-  ( A. y e. On ~P ( aleph ` y ) e. dom card -> ( -. ( card ` x ) e. _om -> ~P ( card ` x ) e. dom card ) )
23 nnfi 
 |-  ( ( card ` x ) e. _om -> ( card ` x ) e. Fin )
24 pwfi 
 |-  ( ( card ` x ) e. Fin <-> ~P ( card ` x ) e. Fin )
25 23 24 sylib 
 |-  ( ( card ` x ) e. _om -> ~P ( card ` x ) e. Fin )
26 finnum 
 |-  ( ~P ( card ` x ) e. Fin -> ~P ( card ` x ) e. dom card )
27 25 26 syl 
 |-  ( ( card ` x ) e. _om -> ~P ( card ` x ) e. dom card )
28 22 27 pm2.61d2 
 |-  ( A. y e. On ~P ( aleph ` y ) e. dom card -> ~P ( card ` x ) e. dom card )
29 oncardid 
 |-  ( x e. On -> ( card ` x ) ~~ x )
30 pwen 
 |-  ( ( card ` x ) ~~ x -> ~P ( card ` x ) ~~ ~P x )
31 ennum 
 |-  ( ~P ( card ` x ) ~~ ~P x -> ( ~P ( card ` x ) e. dom card <-> ~P x e. dom card ) )
32 29 30 31 3syl 
 |-  ( x e. On -> ( ~P ( card ` x ) e. dom card <-> ~P x e. dom card ) )
33 28 32 syl5ibcom 
 |-  ( A. y e. On ~P ( aleph ` y ) e. dom card -> ( x e. On -> ~P x e. dom card ) )
34 33 ralrimiv 
 |-  ( A. y e. On ~P ( aleph ` y ) e. dom card -> A. x e. On ~P x e. dom card )
35 6 34 impbii 
 |-  ( A. x e. On ~P x e. dom card <-> A. y e. On ~P ( aleph ` y ) e. dom card )