Metamath Proof Explorer

Theorem dfac2a

Description: Our Axiom of Choice (in the form of ac3 ) implies the Axiom of Choice (first form) of Enderton p. 49. The proof uses neither AC nor the Axiom of Regularity. See dfac2b for the converse (which does use the Axiom of Regularity). (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion dfac2a 
|- ( A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> CHOICE )

Proof

Step Hyp Ref Expression
1 riotauni 
 |-  ( E! w e. z E. v e. y ( z e. v /\ w e. v ) -> ( iota_ w e. z E. v e. y ( z e. v /\ w e. v ) ) = U. { w e. z | E. v e. y ( z e. v /\ w e. v ) } )
2 riotacl 
 |-  ( E! w e. z E. v e. y ( z e. v /\ w e. v ) -> ( iota_ w e. z E. v e. y ( z e. v /\ w e. v ) ) e. z )
3 1 2 eqeltrrd 
 |-  ( E! w e. z E. v e. y ( z e. v /\ w e. v ) -> U. { w e. z | E. v e. y ( z e. v /\ w e. v ) } e. z )
4 elequ2 
 |-  ( u = z -> ( w e. u <-> w e. z ) )
5 elequ1 
 |-  ( u = z -> ( u e. v <-> z e. v ) )
6 5 anbi1d 
 |-  ( u = z -> ( ( u e. v /\ w e. v ) <-> ( z e. v /\ w e. v ) ) )
7 6 rexbidv 
 |-  ( u = z -> ( E. v e. y ( u e. v /\ w e. v ) <-> E. v e. y ( z e. v /\ w e. v ) ) )
8 4 7 anbi12d 
 |-  ( u = z -> ( ( w e. u /\ E. v e. y ( u e. v /\ w e. v ) ) <-> ( w e. z /\ E. v e. y ( z e. v /\ w e. v ) ) ) )
9 8 rabbidva2 
 |-  ( u = z -> { w e. u | E. v e. y ( u e. v /\ w e. v ) } = { w e. z | E. v e. y ( z e. v /\ w e. v ) } )
10 9 unieqd 
 |-  ( u = z -> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } = U. { w e. z | E. v e. y ( z e. v /\ w e. v ) } )
11 eqid 
 |-  ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) = ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } )
12 vex 
 |-  z e. _V
13 12 rabex 
 |-  { w e. z | E. v e. y ( z e. v /\ w e. v ) } e. _V
14 13 uniex 
 |-  U. { w e. z | E. v e. y ( z e. v /\ w e. v ) } e. _V
15 10 11 14 fvmpt 
 |-  ( z e. x -> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) = U. { w e. z | E. v e. y ( z e. v /\ w e. v ) } )
16 15 eleq1d 
 |-  ( z e. x -> ( ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z <-> U. { w e. z | E. v e. y ( z e. v /\ w e. v ) } e. z ) )
17 3 16 syl5ibr 
 |-  ( z e. x -> ( E! w e. z E. v e. y ( z e. v /\ w e. v ) -> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z ) )
18 17 imim2d 
 |-  ( z e. x -> ( ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> ( z =/= (/) -> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z ) ) )
19 18 ralimia 
 |-  ( A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> A. z e. x ( z =/= (/) -> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z ) )
20 ssrab2 
 |-  { w e. u | E. v e. y ( u e. v /\ w e. v ) } C_ u
21 elssuni 
 |-  ( u e. x -> u C_ U. x )
22 20 21 sstrid 
 |-  ( u e. x -> { w e. u | E. v e. y ( u e. v /\ w e. v ) } C_ U. x )
23 22 unissd 
 |-  ( u e. x -> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } C_ U. U. x )
24 vex 
 |-  x e. _V
25 24 uniex 
 |-  U. x e. _V
26 25 uniex 
 |-  U. U. x e. _V
27 26 elpw2 
 |-  ( U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } e. ~P U. U. x <-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } C_ U. U. x )
28 23 27 sylibr 
 |-  ( u e. x -> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } e. ~P U. U. x )
29 11 28 fmpti 
 |-  ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) : x --> ~P U. U. x
30 26 pwex 
 |-  ~P U. U. x e. _V
31 fex2 
 |-  ( ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) : x --> ~P U. U. x /\ x e. _V /\ ~P U. U. x e. _V ) -> ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) e. _V )
32 29 24 30 31 mp3an 
 |-  ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) e. _V
33 fveq1 
 |-  ( f = ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) -> ( f ` z ) = ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) )
34 33 eleq1d 
 |-  ( f = ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) -> ( ( f ` z ) e. z <-> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z ) )
35 34 imbi2d 
 |-  ( f = ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( z =/= (/) -> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z ) ) )
36 35 ralbidv 
 |-  ( f = ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z ) ) )
37 32 36 spcev 
 |-  ( A. z e. x ( z =/= (/) -> ( ( u e. x |-> U. { w e. u | E. v e. y ( u e. v /\ w e. v ) } ) ` z ) e. z ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
38 19 37 syl 
 |-  ( A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
39 38 exlimiv 
 |-  ( E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
40 39 alimi 
 |-  ( A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
41 dfac3 
 |-  ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
42 40 41 sylibr 
 |-  ( A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) -> CHOICE )