Metamath Proof Explorer

Theorem dfac12r

Description: The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion dfac12r 
|- ( A. x e. On ~P x e. dom card <-> U. ( R1 " On ) C_ dom card )

Proof

Step Hyp Ref Expression
1 rankwflemb 
 |-  ( y e. U. ( R1 " On ) <-> E. z e. On y e. ( R1 ` suc z ) )
2 harcl 
 |-  ( har ` ( R1 ` z ) ) e. On
3 pweq 
 |-  ( x = ( har ` ( R1 ` z ) ) -> ~P x = ~P ( har ` ( R1 ` z ) ) )
4 3 eleq1d 
 |-  ( x = ( har ` ( R1 ` z ) ) -> ( ~P x e. dom card <-> ~P ( har ` ( R1 ` z ) ) e. dom card ) )
5 4 rspcv 
 |-  ( ( har ` ( R1 ` z ) ) e. On -> ( A. x e. On ~P x e. dom card -> ~P ( har ` ( R1 ` z ) ) e. dom card ) )
6 2 5 ax-mp 
 |-  ( A. x e. On ~P x e. dom card -> ~P ( har ` ( R1 ` z ) ) e. dom card )
7 cardid2 
 |-  ( ~P ( har ` ( R1 ` z ) ) e. dom card -> ( card ` ~P ( har ` ( R1 ` z ) ) ) ~~ ~P ( har ` ( R1 ` z ) ) )
8 ensym 
 |-  ( ( card ` ~P ( har ` ( R1 ` z ) ) ) ~~ ~P ( har ` ( R1 ` z ) ) -> ~P ( har ` ( R1 ` z ) ) ~~ ( card ` ~P ( har ` ( R1 ` z ) ) ) )
9 bren 
 |-  ( ~P ( har ` ( R1 ` z ) ) ~~ ( card ` ~P ( har ` ( R1 ` z ) ) ) <-> E. f f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) )
10 simpr 
 |-  ( ( f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) /\ z e. On ) -> z e. On )
11 f1of1 
 |-  ( f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) -> f : ~P ( har ` ( R1 ` z ) ) -1-1-> ( card ` ~P ( har ` ( R1 ` z ) ) ) )
12 11 adantr 
 |-  ( ( f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) /\ z e. On ) -> f : ~P ( har ` ( R1 ` z ) ) -1-1-> ( card ` ~P ( har ` ( R1 ` z ) ) ) )
13 cardon 
 |-  ( card ` ~P ( har ` ( R1 ` z ) ) ) e. On
14 13 onssi 
 |-  ( card ` ~P ( har ` ( R1 ` z ) ) ) C_ On
15 f1ss 
 |-  ( ( f : ~P ( har ` ( R1 ` z ) ) -1-1-> ( card ` ~P ( har ` ( R1 ` z ) ) ) /\ ( card ` ~P ( har ` ( R1 ` z ) ) ) C_ On ) -> f : ~P ( har ` ( R1 ` z ) ) -1-1-> On )
16 12 14 15 sylancl 
 |-  ( ( f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) /\ z e. On ) -> f : ~P ( har ` ( R1 ` z ) ) -1-1-> On )
17 fveq2 
 |-  ( y = b -> ( rank ` y ) = ( rank ` b ) )
18 17 oveq2d 
 |-  ( y = b -> ( suc U. ran U. ran x .o ( rank ` y ) ) = ( suc U. ran U. ran x .o ( rank ` b ) ) )
19 suceq 
 |-  ( ( rank ` y ) = ( rank ` b ) -> suc ( rank ` y ) = suc ( rank ` b ) )
20 17 19 syl 
 |-  ( y = b -> suc ( rank ` y ) = suc ( rank ` b ) )
21 20 fveq2d 
 |-  ( y = b -> ( x ` suc ( rank ` y ) ) = ( x ` suc ( rank ` b ) ) )
22 id 
 |-  ( y = b -> y = b )
23 21 22 fveq12d 
 |-  ( y = b -> ( ( x ` suc ( rank ` y ) ) ` y ) = ( ( x ` suc ( rank ` b ) ) ` b ) )
24 18 23 oveq12d 
 |-  ( y = b -> ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ran x .o ( rank ` b ) ) +o ( ( x ` suc ( rank ` b ) ) ` b ) ) )
25 imaeq2 
 |-  ( y = b -> ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) = ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) )
26 25 fveq2d 
 |-  ( y = b -> ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) = ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) ) )
27 24 26 ifeq12d 
 |-  ( y = b -> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) = if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` b ) ) +o ( ( x ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) ) ) )
28 27 cbvmptv 
 |-  ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) = ( b e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` b ) ) +o ( ( x ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) ) ) )
29 dmeq 
 |-  ( x = a -> dom x = dom a )
30 29 fveq2d 
 |-  ( x = a -> ( R1 ` dom x ) = ( R1 ` dom a ) )
31 29 unieqd 
 |-  ( x = a -> U. dom x = U. dom a )
32 29 31 eqeq12d 
 |-  ( x = a -> ( dom x = U. dom x <-> dom a = U. dom a ) )
33 rneq 
 |-  ( x = a -> ran x = ran a )
34 33 unieqd 
 |-  ( x = a -> U. ran x = U. ran a )
35 34 rneqd 
 |-  ( x = a -> ran U. ran x = ran U. ran a )
36 35 unieqd 
 |-  ( x = a -> U. ran U. ran x = U. ran U. ran a )
37 suceq 
 |-  ( U. ran U. ran x = U. ran U. ran a -> suc U. ran U. ran x = suc U. ran U. ran a )
38 36 37 syl 
 |-  ( x = a -> suc U. ran U. ran x = suc U. ran U. ran a )
39 38 oveq1d 
 |-  ( x = a -> ( suc U. ran U. ran x .o ( rank ` b ) ) = ( suc U. ran U. ran a .o ( rank ` b ) ) )
40 fveq1 
 |-  ( x = a -> ( x ` suc ( rank ` b ) ) = ( a ` suc ( rank ` b ) ) )
41 40 fveq1d 
 |-  ( x = a -> ( ( x ` suc ( rank ` b ) ) ` b ) = ( ( a ` suc ( rank ` b ) ) ` b ) )
42 39 41 oveq12d 
 |-  ( x = a -> ( ( suc U. ran U. ran x .o ( rank ` b ) ) +o ( ( x ` suc ( rank ` b ) ) ` b ) ) = ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) )
43 id 
 |-  ( x = a -> x = a )
44 43 31 fveq12d 
 |-  ( x = a -> ( x ` U. dom x ) = ( a ` U. dom a ) )
45 44 rneqd 
 |-  ( x = a -> ran ( x ` U. dom x ) = ran ( a ` U. dom a ) )
46 oieq2 
 |-  ( ran ( x ` U. dom x ) = ran ( a ` U. dom a ) -> OrdIso ( _E , ran ( x ` U. dom x ) ) = OrdIso ( _E , ran ( a ` U. dom a ) ) )
47 45 46 syl 
 |-  ( x = a -> OrdIso ( _E , ran ( x ` U. dom x ) ) = OrdIso ( _E , ran ( a ` U. dom a ) ) )
48 47 cnveqd 
 |-  ( x = a -> `' OrdIso ( _E , ran ( x ` U. dom x ) ) = `' OrdIso ( _E , ran ( a ` U. dom a ) ) )
49 48 44 coeq12d 
 |-  ( x = a -> ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) = ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) )
50 49 imaeq1d 
 |-  ( x = a -> ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) = ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) )
51 50 fveq2d 
 |-  ( x = a -> ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) ) = ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) )
52 32 42 51 ifbieq12d 
 |-  ( x = a -> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` b ) ) +o ( ( x ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) ) ) = if ( dom a = U. dom a , ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) ) )
53 30 52 mpteq12dv 
 |-  ( x = a -> ( b e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` b ) ) +o ( ( x ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " b ) ) ) ) = ( b e. ( R1 ` dom a ) |-> if ( dom a = U. dom a , ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) ) ) )
54 28 53 eqtrid 
 |-  ( x = a -> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) = ( b e. ( R1 ` dom a ) |-> if ( dom a = U. dom a , ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) ) ) )
55 54 cbvmptv 
 |-  ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) = ( a e. _V |-> ( b e. ( R1 ` dom a ) |-> if ( dom a = U. dom a , ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) ) ) )
56 recseq 
 |-  ( ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) = ( a e. _V |-> ( b e. ( R1 ` dom a ) |-> if ( dom a = U. dom a , ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) ) ) ) -> recs ( ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) ) = recs ( ( a e. _V |-> ( b e. ( R1 ` dom a ) |-> if ( dom a = U. dom a , ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) ) ) ) ) )
57 55 56 ax-mp 
 |-  recs ( ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) ) = recs ( ( a e. _V |-> ( b e. ( R1 ` dom a ) |-> if ( dom a = U. dom a , ( ( suc U. ran U. ran a .o ( rank ` b ) ) +o ( ( a ` suc ( rank ` b ) ) ` b ) ) , ( f ` ( ( `' OrdIso ( _E , ran ( a ` U. dom a ) ) o. ( a ` U. dom a ) ) " b ) ) ) ) ) )
58 10 16 57 dfac12lem3 
 |-  ( ( f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) /\ z e. On ) -> ( R1 ` z ) e. dom card )
59 58 ex 
 |-  ( f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) -> ( z e. On -> ( R1 ` z ) e. dom card ) )
60 59 exlimiv 
 |-  ( E. f f : ~P ( har ` ( R1 ` z ) ) -1-1-onto-> ( card ` ~P ( har ` ( R1 ` z ) ) ) -> ( z e. On -> ( R1 ` z ) e. dom card ) )
61 9 60 sylbi 
 |-  ( ~P ( har ` ( R1 ` z ) ) ~~ ( card ` ~P ( har ` ( R1 ` z ) ) ) -> ( z e. On -> ( R1 ` z ) e. dom card ) )
62 6 7 8 61 4syl 
 |-  ( A. x e. On ~P x e. dom card -> ( z e. On -> ( R1 ` z ) e. dom card ) )
63 62 imp 
 |-  ( ( A. x e. On ~P x e. dom card /\ z e. On ) -> ( R1 ` z ) e. dom card )
64 r1suc 
 |-  ( z e. On -> ( R1 ` suc z ) = ~P ( R1 ` z ) )
65 64 adantl 
 |-  ( ( A. x e. On ~P x e. dom card /\ z e. On ) -> ( R1 ` suc z ) = ~P ( R1 ` z ) )
66 65 eleq2d 
 |-  ( ( A. x e. On ~P x e. dom card /\ z e. On ) -> ( y e. ( R1 ` suc z ) <-> y e. ~P ( R1 ` z ) ) )
67 elpwi 
 |-  ( y e. ~P ( R1 ` z ) -> y C_ ( R1 ` z ) )
68 66 67 syl6bi 
 |-  ( ( A. x e. On ~P x e. dom card /\ z e. On ) -> ( y e. ( R1 ` suc z ) -> y C_ ( R1 ` z ) ) )
69 ssnum 
 |-  ( ( ( R1 ` z ) e. dom card /\ y C_ ( R1 ` z ) ) -> y e. dom card )
70 63 68 69 syl6an 
 |-  ( ( A. x e. On ~P x e. dom card /\ z e. On ) -> ( y e. ( R1 ` suc z ) -> y e. dom card ) )
71 70 rexlimdva 
 |-  ( A. x e. On ~P x e. dom card -> ( E. z e. On y e. ( R1 ` suc z ) -> y e. dom card ) )
72 1 71 syl5bi 
 |-  ( A. x e. On ~P x e. dom card -> ( y e. U. ( R1 " On ) -> y e. dom card ) )
73 72 ssrdv 
 |-  ( A. x e. On ~P x e. dom card -> U. ( R1 " On ) C_ dom card )
74 onwf 
 |-  On C_ U. ( R1 " On )
75 74 sseli 
 |-  ( x e. On -> x e. U. ( R1 " On ) )
76 pwwf 
 |-  ( x e. U. ( R1 " On ) <-> ~P x e. U. ( R1 " On ) )
77 75 76 sylib 
 |-  ( x e. On -> ~P x e. U. ( R1 " On ) )
78 ssel 
 |-  ( U. ( R1 " On ) C_ dom card -> ( ~P x e. U. ( R1 " On ) -> ~P x e. dom card ) )
79 77 78 syl5 
 |-  ( U. ( R1 " On ) C_ dom card -> ( x e. On -> ~P x e. dom card ) )
80 79 ralrimiv 
 |-  ( U. ( R1 " On ) C_ dom card -> A. x e. On ~P x e. dom card )
81 73 80 impbii 
 |-  ( A. x e. On ~P x e. dom card <-> U. ( R1 " On ) C_ dom card )