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 ) )