Metamath Proof Explorer

Theorem ac6num

Description: A version of ac6 which takes the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis ac6num.1 
|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion ac6num 
|- ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )

Proof

Step Hyp Ref Expression
1 ac6num.1 
 |-  ( y = ( f ` x ) -> ( ph <-> ps ) )
2 nfiu1 
 |-  F/_ x U_ x e. A { y e. B | ph }
3 2 nfel1 
 |-  F/ x U_ x e. A { y e. B | ph } e. dom card
4 ssiun2 
 |-  ( x e. A -> { y e. B | ph } C_ U_ x e. A { y e. B | ph } )
5 ssexg 
 |-  ( ( { y e. B | ph } C_ U_ x e. A { y e. B | ph } /\ U_ x e. A { y e. B | ph } e. dom card ) -> { y e. B | ph } e. _V )
6 5 expcom 
 |-  ( U_ x e. A { y e. B | ph } e. dom card -> ( { y e. B | ph } C_ U_ x e. A { y e. B | ph } -> { y e. B | ph } e. _V ) )
7 4 6 syl5 
 |-  ( U_ x e. A { y e. B | ph } e. dom card -> ( x e. A -> { y e. B | ph } e. _V ) )
8 3 7 ralrimi 
 |-  ( U_ x e. A { y e. B | ph } e. dom card -> A. x e. A { y e. B | ph } e. _V )
9 dfiun2g 
 |-  ( A. x e. A { y e. B | ph } e. _V -> U_ x e. A { y e. B | ph } = U. { z | E. x e. A z = { y e. B | ph } } )
10 8 9 syl 
 |-  ( U_ x e. A { y e. B | ph } e. dom card -> U_ x e. A { y e. B | ph } = U. { z | E. x e. A z = { y e. B | ph } } )
11 eqid 
 |-  ( x e. A |-> { y e. B | ph } ) = ( x e. A |-> { y e. B | ph } )
12 11 rnmpt 
 |-  ran ( x e. A |-> { y e. B | ph } ) = { z | E. x e. A z = { y e. B | ph } }
13 12 unieqi 
 |-  U. ran ( x e. A |-> { y e. B | ph } ) = U. { z | E. x e. A z = { y e. B | ph } }
14 10 13 eqtr4di 
 |-  ( U_ x e. A { y e. B | ph } e. dom card -> U_ x e. A { y e. B | ph } = U. ran ( x e. A |-> { y e. B | ph } ) )
15 id 
 |-  ( U_ x e. A { y e. B | ph } e. dom card -> U_ x e. A { y e. B | ph } e. dom card )
16 14 15 eqeltrrd 
 |-  ( U_ x e. A { y e. B | ph } e. dom card -> U. ran ( x e. A |-> { y e. B | ph } ) e. dom card )
17 16 3ad2ant2 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> U. ran ( x e. A |-> { y e. B | ph } ) e. dom card )
18 simp3 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> A. x e. A E. y e. B ph )
19 necom 
 |-  ( { y e. B | ph } =/= (/) <-> (/) =/= { y e. B | ph } )
20 rabn0 
 |-  ( { y e. B | ph } =/= (/) <-> E. y e. B ph )
21 df-ne 
 |-  ( (/) =/= { y e. B | ph } <-> -. (/) = { y e. B | ph } )
22 19 20 21 3bitr3i 
 |-  ( E. y e. B ph <-> -. (/) = { y e. B | ph } )
23 22 ralbii 
 |-  ( A. x e. A E. y e. B ph <-> A. x e. A -. (/) = { y e. B | ph } )
24 ralnex 
 |-  ( A. x e. A -. (/) = { y e. B | ph } <-> -. E. x e. A (/) = { y e. B | ph } )
25 23 24 bitri 
 |-  ( A. x e. A E. y e. B ph <-> -. E. x e. A (/) = { y e. B | ph } )
26 18 25 sylib 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> -. E. x e. A (/) = { y e. B | ph } )
27 0ex 
 |-  (/) e. _V
28 11 elrnmpt 
 |-  ( (/) e. _V -> ( (/) e. ran ( x e. A |-> { y e. B | ph } ) <-> E. x e. A (/) = { y e. B | ph } ) )
29 27 28 ax-mp 
 |-  ( (/) e. ran ( x e. A |-> { y e. B | ph } ) <-> E. x e. A (/) = { y e. B | ph } )
30 26 29 sylnibr 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> -. (/) e. ran ( x e. A |-> { y e. B | ph } ) )
31 ac5num 
 |-  ( ( U. ran ( x e. A |-> { y e. B | ph } ) e. dom card /\ -. (/) e. ran ( x e. A |-> { y e. B | ph } ) ) -> E. g ( g : ran ( x e. A |-> { y e. B | ph } ) --> U. ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) )
32 17 30 31 syl2anc 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> E. g ( g : ran ( x e. A |-> { y e. B | ph } ) --> U. ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) )
33 ffn 
 |-  ( g : ran ( x e. A |-> { y e. B | ph } ) --> U. ran ( x e. A |-> { y e. B | ph } ) -> g Fn ran ( x e. A |-> { y e. B | ph } ) )
34 33 anim1i 
 |-  ( ( g : ran ( x e. A |-> { y e. B | ph } ) --> U. ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) -> ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) )
35 8 3ad2ant2 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> A. x e. A { y e. B | ph } e. _V )
36 fveq2 
 |-  ( z = { y e. B | ph } -> ( g ` z ) = ( g ` { y e. B | ph } ) )
37 id 
 |-  ( z = { y e. B | ph } -> z = { y e. B | ph } )
38 36 37 eleq12d 
 |-  ( z = { y e. B | ph } -> ( ( g ` z ) e. z <-> ( g ` { y e. B | ph } ) e. { y e. B | ph } ) )
39 11 38 ralrnmptw 
 |-  ( A. x e. A { y e. B | ph } e. _V -> ( A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z <-> A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) )
40 35 39 syl 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> ( A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z <-> A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) )
41 40 anbi2d 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> ( ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) <-> ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) )
42 34 41 syl5ib 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> ( ( g : ran ( x e. A |-> { y e. B | ph } ) --> U. ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) -> ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) )
43 simpl1 
 |-  ( ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) /\ ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) -> A e. V )
44 43 mptexd 
 |-  ( ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) /\ ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) -> ( x e. A |-> ( g ` { y e. B | ph } ) ) e. _V )
45 elrabi 
 |-  ( ( g ` { y e. B | ph } ) e. { y e. B | ph } -> ( g ` { y e. B | ph } ) e. B )
46 45 ralimi 
 |-  ( A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } -> A. x e. A ( g ` { y e. B | ph } ) e. B )
47 46 ad2antll 
 |-  ( ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) /\ ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) -> A. x e. A ( g ` { y e. B | ph } ) e. B )
48 eqid 
 |-  ( x e. A |-> ( g ` { y e. B | ph } ) ) = ( x e. A |-> ( g ` { y e. B | ph } ) )
49 48 fmpt 
 |-  ( A. x e. A ( g ` { y e. B | ph } ) e. B <-> ( x e. A |-> ( g ` { y e. B | ph } ) ) : A --> B )
50 47 49 sylib 
 |-  ( ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) /\ ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) -> ( x e. A |-> ( g ` { y e. B | ph } ) ) : A --> B )
51 nfcv 
 |-  F/_ y B
52 51 elrabsf 
 |-  ( ( g ` { y e. B | ph } ) e. { y e. B | ph } <-> ( ( g ` { y e. B | ph } ) e. B /\ [. ( g ` { y e. B | ph } ) / y ]. ph ) )
53 52 simprbi 
 |-  ( ( g ` { y e. B | ph } ) e. { y e. B | ph } -> [. ( g ` { y e. B | ph } ) / y ]. ph )
54 53 ralimi 
 |-  ( A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } -> A. x e. A [. ( g ` { y e. B | ph } ) / y ]. ph )
55 54 ad2antll 
 |-  ( ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) /\ ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) -> A. x e. A [. ( g ` { y e. B | ph } ) / y ]. ph )
56 50 55 jca 
 |-  ( ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) /\ ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) -> ( ( x e. A |-> ( g ` { y e. B | ph } ) ) : A --> B /\ A. x e. A [. ( g ` { y e. B | ph } ) / y ]. ph ) )
57 feq1 
 |-  ( f = ( x e. A |-> ( g ` { y e. B | ph } ) ) -> ( f : A --> B <-> ( x e. A |-> ( g ` { y e. B | ph } ) ) : A --> B ) )
58 nfmpt1 
 |-  F/_ x ( x e. A |-> ( g ` { y e. B | ph } ) )
59 58 nfeq2 
 |-  F/ x f = ( x e. A |-> ( g ` { y e. B | ph } ) )
60 fvex 
 |-  ( f ` x ) e. _V
61 60 1 sbcie 
 |-  ( [. ( f ` x ) / y ]. ph <-> ps )
62 fveq1 
 |-  ( f = ( x e. A |-> ( g ` { y e. B | ph } ) ) -> ( f ` x ) = ( ( x e. A |-> ( g ` { y e. B | ph } ) ) ` x ) )
63 fvex 
 |-  ( g ` { y e. B | ph } ) e. _V
64 48 fvmpt2 
 |-  ( ( x e. A /\ ( g ` { y e. B | ph } ) e. _V ) -> ( ( x e. A |-> ( g ` { y e. B | ph } ) ) ` x ) = ( g ` { y e. B | ph } ) )
65 63 64 mpan2 
 |-  ( x e. A -> ( ( x e. A |-> ( g ` { y e. B | ph } ) ) ` x ) = ( g ` { y e. B | ph } ) )
66 62 65 sylan9eq 
 |-  ( ( f = ( x e. A |-> ( g ` { y e. B | ph } ) ) /\ x e. A ) -> ( f ` x ) = ( g ` { y e. B | ph } ) )
67 66 sbceq1d 
 |-  ( ( f = ( x e. A |-> ( g ` { y e. B | ph } ) ) /\ x e. A ) -> ( [. ( f ` x ) / y ]. ph <-> [. ( g ` { y e. B | ph } ) / y ]. ph ) )
68 61 67 bitr3id 
 |-  ( ( f = ( x e. A |-> ( g ` { y e. B | ph } ) ) /\ x e. A ) -> ( ps <-> [. ( g ` { y e. B | ph } ) / y ]. ph ) )
69 59 68 ralbida 
 |-  ( f = ( x e. A |-> ( g ` { y e. B | ph } ) ) -> ( A. x e. A ps <-> A. x e. A [. ( g ` { y e. B | ph } ) / y ]. ph ) )
70 57 69 anbi12d 
 |-  ( f = ( x e. A |-> ( g ` { y e. B | ph } ) ) -> ( ( f : A --> B /\ A. x e. A ps ) <-> ( ( x e. A |-> ( g ` { y e. B | ph } ) ) : A --> B /\ A. x e. A [. ( g ` { y e. B | ph } ) / y ]. ph ) ) )
71 44 56 70 spcedv 
 |-  ( ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) /\ ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) ) -> E. f ( f : A --> B /\ A. x e. A ps ) )
72 71 ex 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> ( ( g Fn ran ( x e. A |-> { y e. B | ph } ) /\ A. x e. A ( g ` { y e. B | ph } ) e. { y e. B | ph } ) -> E. f ( f : A --> B /\ A. x e. A ps ) ) )
73 42 72 syld 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> ( ( g : ran ( x e. A |-> { y e. B | ph } ) --> U. ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) -> E. f ( f : A --> B /\ A. x e. A ps ) ) )
74 73 exlimdv 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> ( E. g ( g : ran ( x e. A |-> { y e. B | ph } ) --> U. ran ( x e. A |-> { y e. B | ph } ) /\ A. z e. ran ( x e. A |-> { y e. B | ph } ) ( g ` z ) e. z ) -> E. f ( f : A --> B /\ A. x e. A ps ) ) )
75 32 74 mpd 
 |-  ( ( A e. V /\ U_ x e. A { y e. B | ph } e. dom card /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )