Metamath Proof Explorer

Theorem dfacacn

Description: A choice equivalent: every set has choice sets of every length. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dfacacn 
|- ( CHOICE <-> A. x AC_ x = _V )

Proof

Step Hyp Ref Expression
1 acacni 
 |-  ( ( CHOICE /\ x e. _V ) -> AC_ x = _V )
2 1 elvd 
 |-  ( CHOICE -> AC_ x = _V )
3 2 alrimiv 
 |-  ( CHOICE -> A. x AC_ x = _V )
4 vex 
 |-  y e. _V
5 4 difexi 
 |-  ( y \ { (/) } ) e. _V
6 acneq 
 |-  ( x = ( y \ { (/) } ) -> AC_ x = AC_ ( y \ { (/) } ) )
7 6 eqeq1d 
 |-  ( x = ( y \ { (/) } ) -> ( AC_ x = _V <-> AC_ ( y \ { (/) } ) = _V ) )
8 5 7 spcv 
 |-  ( A. x AC_ x = _V -> AC_ ( y \ { (/) } ) = _V )
9 vuniex 
 |-  U. y e. _V
10 id 
 |-  ( AC_ ( y \ { (/) } ) = _V -> AC_ ( y \ { (/) } ) = _V )
11 9 10 eleqtrrid 
 |-  ( AC_ ( y \ { (/) } ) = _V -> U. y e. AC_ ( y \ { (/) } ) )
12 eldifi 
 |-  ( z e. ( y \ { (/) } ) -> z e. y )
13 elssuni 
 |-  ( z e. y -> z C_ U. y )
14 12 13 syl 
 |-  ( z e. ( y \ { (/) } ) -> z C_ U. y )
15 eldifsni 
 |-  ( z e. ( y \ { (/) } ) -> z =/= (/) )
16 14 15 jca 
 |-  ( z e. ( y \ { (/) } ) -> ( z C_ U. y /\ z =/= (/) ) )
17 16 rgen 
 |-  A. z e. ( y \ { (/) } ) ( z C_ U. y /\ z =/= (/) )
18 acni2 
 |-  ( ( U. y e. AC_ ( y \ { (/) } ) /\ A. z e. ( y \ { (/) } ) ( z C_ U. y /\ z =/= (/) ) ) -> E. g ( g : ( y \ { (/) } ) --> U. y /\ A. z e. ( y \ { (/) } ) ( g ` z ) e. z ) )
19 11 17 18 sylancl 
 |-  ( AC_ ( y \ { (/) } ) = _V -> E. g ( g : ( y \ { (/) } ) --> U. y /\ A. z e. ( y \ { (/) } ) ( g ` z ) e. z ) )
20 4 mptex 
 |-  ( x e. y |-> ( g ` x ) ) e. _V
21 simpr 
 |-  ( ( g : ( y \ { (/) } ) --> U. y /\ A. z e. ( y \ { (/) } ) ( g ` z ) e. z ) -> A. z e. ( y \ { (/) } ) ( g ` z ) e. z )
22 eldifsn 
 |-  ( z e. ( y \ { (/) } ) <-> ( z e. y /\ z =/= (/) ) )
23 22 imbi1i 
 |-  ( ( z e. ( y \ { (/) } ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) <-> ( ( z e. y /\ z =/= (/) ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) )
24 fveq2 
 |-  ( x = z -> ( g ` x ) = ( g ` z ) )
25 eqid 
 |-  ( x e. y |-> ( g ` x ) ) = ( x e. y |-> ( g ` x ) )
26 fvex 
 |-  ( g ` z ) e. _V
27 24 25 26 fvmpt 
 |-  ( z e. y -> ( ( x e. y |-> ( g ` x ) ) ` z ) = ( g ` z ) )
28 12 27 syl 
 |-  ( z e. ( y \ { (/) } ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) = ( g ` z ) )
29 28 eleq1d 
 |-  ( z e. ( y \ { (/) } ) -> ( ( ( x e. y |-> ( g ` x ) ) ` z ) e. z <-> ( g ` z ) e. z ) )
30 29 pm5.74i 
 |-  ( ( z e. ( y \ { (/) } ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) <-> ( z e. ( y \ { (/) } ) -> ( g ` z ) e. z ) )
31 impexp 
 |-  ( ( ( z e. y /\ z =/= (/) ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) <-> ( z e. y -> ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) )
32 23 30 31 3bitr3i 
 |-  ( ( z e. ( y \ { (/) } ) -> ( g ` z ) e. z ) <-> ( z e. y -> ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) )
33 32 ralbii2 
 |-  ( A. z e. ( y \ { (/) } ) ( g ` z ) e. z <-> A. z e. y ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) )
34 21 33 sylib 
 |-  ( ( g : ( y \ { (/) } ) --> U. y /\ A. z e. ( y \ { (/) } ) ( g ` z ) e. z ) -> A. z e. y ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) )
35 fvrn0 
 |-  ( g ` x ) e. ( ran g u. { (/) } )
36 35 rgenw 
 |-  A. x e. y ( g ` x ) e. ( ran g u. { (/) } )
37 25 fmpt 
 |-  ( A. x e. y ( g ` x ) e. ( ran g u. { (/) } ) <-> ( x e. y |-> ( g ` x ) ) : y --> ( ran g u. { (/) } ) )
38 36 37 mpbi 
 |-  ( x e. y |-> ( g ` x ) ) : y --> ( ran g u. { (/) } )
39 ffn 
 |-  ( ( x e. y |-> ( g ` x ) ) : y --> ( ran g u. { (/) } ) -> ( x e. y |-> ( g ` x ) ) Fn y )
40 38 39 ax-mp 
 |-  ( x e. y |-> ( g ` x ) ) Fn y
41 34 40 jctil 
 |-  ( ( g : ( y \ { (/) } ) --> U. y /\ A. z e. ( y \ { (/) } ) ( g ` z ) e. z ) -> ( ( x e. y |-> ( g ` x ) ) Fn y /\ A. z e. y ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) )
42 fneq1 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( f Fn y <-> ( x e. y |-> ( g ` x ) ) Fn y ) )
43 fveq1 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( f ` z ) = ( ( x e. y |-> ( g ` x ) ) ` z ) )
44 43 eleq1d 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( ( f ` z ) e. z <-> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) )
45 44 imbi2d 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) )
46 45 ralbidv 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. y ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) )
47 42 46 anbi12d 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) <-> ( ( x e. y |-> ( g ` x ) ) Fn y /\ A. z e. y ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) ) )
48 47 spcegv 
 |-  ( ( x e. y |-> ( g ` x ) ) e. _V -> ( ( ( x e. y |-> ( g ` x ) ) Fn y /\ A. z e. y ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) -> E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) ) )
49 20 41 48 mpsyl 
 |-  ( ( g : ( y \ { (/) } ) --> U. y /\ A. z e. ( y \ { (/) } ) ( g ` z ) e. z ) -> E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
50 49 exlimiv 
 |-  ( E. g ( g : ( y \ { (/) } ) --> U. y /\ A. z e. ( y \ { (/) } ) ( g ` z ) e. z ) -> E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
51 8 19 50 3syl 
 |-  ( A. x AC_ x = _V -> E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
52 51 alrimiv 
 |-  ( A. x AC_ x = _V -> A. y E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
53 dfac4 
 |-  ( CHOICE <-> A. y E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
54 52 53 sylibr 
 |-  ( A. x AC_ x = _V -> CHOICE )
55 3 54 impbii 
 |-  ( CHOICE <-> A. x AC_ x = _V )