Metamath Proof Explorer

Theorem ac5num

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

Ref Expression
Assertion ac5num 
|- ( ( U. A e. dom card /\ -. (/) e. A ) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) )

Proof

Step Hyp Ref Expression
1 uniexr 
 |-  ( U. A e. dom card -> A e. _V )
2 dfac8b 
 |-  ( U. A e. dom card -> E. r r We U. A )
3 dfac8c 
 |-  ( A e. _V -> ( E. r r We U. A -> E. g A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) )
4 1 2 3 sylc 
 |-  ( U. A e. dom card -> E. g A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) )
5 4 adantr 
 |-  ( ( U. A e. dom card /\ -. (/) e. A ) -> E. g A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) )
6 1 ad2antrr 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> A e. _V )
7 6 mptexd 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> ( y e. A |-> ( g ` y ) ) e. _V )
8 nelne2 
 |-  ( ( x e. A /\ -. (/) e. A ) -> x =/= (/) )
9 8 ancoms 
 |-  ( ( -. (/) e. A /\ x e. A ) -> x =/= (/) )
10 9 adantll 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ x e. A ) -> x =/= (/) )
11 pm2.27 
 |-  ( x =/= (/) -> ( ( x =/= (/) -> ( g ` x ) e. x ) -> ( g ` x ) e. x ) )
12 10 11 syl 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ x e. A ) -> ( ( x =/= (/) -> ( g ` x ) e. x ) -> ( g ` x ) e. x ) )
13 12 ralimdva 
 |-  ( ( U. A e. dom card /\ -. (/) e. A ) -> ( A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) -> A. x e. A ( g ` x ) e. x ) )
14 13 imp 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> A. x e. A ( g ` x ) e. x )
15 fveq2 
 |-  ( x = y -> ( g ` x ) = ( g ` y ) )
16 id 
 |-  ( x = y -> x = y )
17 15 16 eleq12d 
 |-  ( x = y -> ( ( g ` x ) e. x <-> ( g ` y ) e. y ) )
18 17 rspccva 
 |-  ( ( A. x e. A ( g ` x ) e. x /\ y e. A ) -> ( g ` y ) e. y )
19 14 18 sylan 
 |-  ( ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) /\ y e. A ) -> ( g ` y ) e. y )
20 elunii 
 |-  ( ( ( g ` y ) e. y /\ y e. A ) -> ( g ` y ) e. U. A )
21 19 20 sylancom 
 |-  ( ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) /\ y e. A ) -> ( g ` y ) e. U. A )
22 21 fmpttd 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> ( y e. A |-> ( g ` y ) ) : A --> U. A )
23 fveq2 
 |-  ( y = x -> ( g ` y ) = ( g ` x ) )
24 eqid 
 |-  ( y e. A |-> ( g ` y ) ) = ( y e. A |-> ( g ` y ) )
25 fvex 
 |-  ( g ` x ) e. _V
26 23 24 25 fvmpt 
 |-  ( x e. A -> ( ( y e. A |-> ( g ` y ) ) ` x ) = ( g ` x ) )
27 26 eleq1d 
 |-  ( x e. A -> ( ( ( y e. A |-> ( g ` y ) ) ` x ) e. x <-> ( g ` x ) e. x ) )
28 27 ralbiia 
 |-  ( A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x <-> A. x e. A ( g ` x ) e. x )
29 14 28 sylibr 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x )
30 22 29 jca 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> ( ( y e. A |-> ( g ` y ) ) : A --> U. A /\ A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) )
31 feq1 
 |-  ( f = ( y e. A |-> ( g ` y ) ) -> ( f : A --> U. A <-> ( y e. A |-> ( g ` y ) ) : A --> U. A ) )
32 fveq1 
 |-  ( f = ( y e. A |-> ( g ` y ) ) -> ( f ` x ) = ( ( y e. A |-> ( g ` y ) ) ` x ) )
33 32 eleq1d 
 |-  ( f = ( y e. A |-> ( g ` y ) ) -> ( ( f ` x ) e. x <-> ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) )
34 33 ralbidv 
 |-  ( f = ( y e. A |-> ( g ` y ) ) -> ( A. x e. A ( f ` x ) e. x <-> A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) )
35 31 34 anbi12d 
 |-  ( f = ( y e. A |-> ( g ` y ) ) -> ( ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) <-> ( ( y e. A |-> ( g ` y ) ) : A --> U. A /\ A. x e. A ( ( y e. A |-> ( g ` y ) ) ` x ) e. x ) ) )
36 7 30 35 spcedv 
 |-  ( ( ( U. A e. dom card /\ -. (/) e. A ) /\ A. x e. A ( x =/= (/) -> ( g ` x ) e. x ) ) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) )
37 5 36 exlimddv 
 |-  ( ( U. A e. dom card /\ -. (/) e. A ) -> E. f ( f : A --> U. A /\ A. x e. A ( f ` x ) e. x ) )