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 eldifsn 
 |-  ( z e. ( y \ { (/) } ) <-> ( z e. y /\ z =/= (/) ) )
22 21 imbi1i 
 |-  ( ( z e. ( y \ { (/) } ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) <-> ( ( z e. y /\ z =/= (/) ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) )
23 fveq2 
 |-  ( x = z -> ( g ` x ) = ( g ` z ) )
24 eqid 
 |-  ( x e. y |-> ( g ` x ) ) = ( x e. y |-> ( g ` x ) )
25 fvex 
 |-  ( g ` z ) e. _V
26 23 24 25 fvmpt 
 |-  ( z e. y -> ( ( x e. y |-> ( g ` x ) ) ` z ) = ( g ` z ) )
27 12 26 syl 
 |-  ( z e. ( y \ { (/) } ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) = ( g ` z ) )
28 27 eleq1d 
 |-  ( z e. ( y \ { (/) } ) -> ( ( ( x e. y |-> ( g ` x ) ) ` z ) e. z <-> ( g ` z ) e. z ) )
29 28 pm5.74i 
 |-  ( ( z e. ( y \ { (/) } ) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) <-> ( z e. ( y \ { (/) } ) -> ( g ` z ) e. z ) )
30 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 ) ) )
31 22 29 30 3bitr3i 
 |-  ( ( z e. ( y \ { (/) } ) -> ( g ` z ) e. z ) <-> ( z e. y -> ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) )
32 31 ralbii2 
 |-  ( A. z e. ( y \ { (/) } ) ( g ` z ) e. z <-> A. z e. y ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) )
33 32 bilani 
 |-  ( ( 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 ) )
34 fvrn0 
 |-  ( g ` x ) e. ( ran g u. { (/) } )
35 34 rgenw 
 |-  A. x e. y ( g ` x ) e. ( ran g u. { (/) } )
36 24 fmpt 
 |-  ( A. x e. y ( g ` x ) e. ( ran g u. { (/) } ) <-> ( x e. y |-> ( g ` x ) ) : y --> ( ran g u. { (/) } ) )
37 35 36 mpbi 
 |-  ( x e. y |-> ( g ` x ) ) : y --> ( ran g u. { (/) } )
38 ffn 
 |-  ( ( x e. y |-> ( g ` x ) ) : y --> ( ran g u. { (/) } ) -> ( x e. y |-> ( g ` x ) ) Fn y )
39 37 38 ax-mp 
 |-  ( x e. y |-> ( g ` x ) ) Fn y
40 33 39 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 ) ) )
41 fneq1 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( f Fn y <-> ( x e. y |-> ( g ` x ) ) Fn y ) )
42 fveq1 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( f ` z ) = ( ( x e. y |-> ( g ` x ) ) ` z ) )
43 42 eleq1d 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( ( f ` z ) e. z <-> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) )
44 43 imbi2d 
 |-  ( f = ( x e. y |-> ( g ` x ) ) -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( z =/= (/) -> ( ( x e. y |-> ( g ` x ) ) ` z ) e. z ) ) )
45 44 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 ) ) )
46 41 45 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 ) ) ) )
47 46 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 ) ) ) )
48 20 40 47 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 ) ) )
49 48 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 ) ) )
50 8 19 49 3syl 
 |-  ( A. x AC_ x = _V -> E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
51 50 alrimiv 
 |-  ( A. x AC_ x = _V -> A. y E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
52 dfac4 
 |-  ( CHOICE <-> A. y E. f ( f Fn y /\ A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
53 51 52 sylibr 
 |-  ( A. x AC_ x = _V -> CHOICE )
54 3 53 impbii 
 |-  ( CHOICE <-> A. x AC_ x = _V )