Metamath Proof Explorer

Theorem dfac3

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is defined as the Axiom of Choice (first form) of Enderton p. 49. The right-hand side is the Axiom of Choice of TakeutiZaring p. 83. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion dfac3 
|- ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )

Proof

Step Hyp Ref Expression
1 df-ac 
 |-  ( CHOICE <-> A. y E. f ( f C_ y /\ f Fn dom y ) )
2 vex 
 |-  x e. _V
3 vuniex 
 |-  U. x e. _V
4 2 3 xpex 
 |-  ( x X. U. x ) e. _V
5 simpl 
 |-  ( ( w e. x /\ v e. w ) -> w e. x )
6 elunii 
 |-  ( ( v e. w /\ w e. x ) -> v e. U. x )
7 6 ancoms 
 |-  ( ( w e. x /\ v e. w ) -> v e. U. x )
8 5 7 jca 
 |-  ( ( w e. x /\ v e. w ) -> ( w e. x /\ v e. U. x ) )
9 8 ssopab2i 
 |-  { <. w , v >. | ( w e. x /\ v e. w ) } C_ { <. w , v >. | ( w e. x /\ v e. U. x ) }
10 df-xp 
 |-  ( x X. U. x ) = { <. w , v >. | ( w e. x /\ v e. U. x ) }
11 9 10 sseqtrri 
 |-  { <. w , v >. | ( w e. x /\ v e. w ) } C_ ( x X. U. x )
12 4 11 ssexi 
 |-  { <. w , v >. | ( w e. x /\ v e. w ) } e. _V
13 sseq2 
 |-  ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( f C_ y <-> f C_ { <. w , v >. | ( w e. x /\ v e. w ) } ) )
14 dmeq 
 |-  ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> dom y = dom { <. w , v >. | ( w e. x /\ v e. w ) } )
15 14 fneq2d 
 |-  ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( f Fn dom y <-> f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) )
16 13 15 anbi12d 
 |-  ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( f C_ y /\ f Fn dom y ) <-> ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) ) )
17 16 exbidv 
 |-  ( y = { <. w , v >. | ( w e. x /\ v e. w ) } -> ( E. f ( f C_ y /\ f Fn dom y ) <-> E. f ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) ) )
18 12 17 spcv 
 |-  ( A. y E. f ( f C_ y /\ f Fn dom y ) -> E. f ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) )
19 fndm 
 |-  ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } )
20 dmopab 
 |-  dom { <. w , v >. | ( w e. x /\ v e. w ) } = { w | E. v ( w e. x /\ v e. w ) }
21 20 eleq2i 
 |-  ( z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } <-> z e. { w | E. v ( w e. x /\ v e. w ) } )
22 vex 
 |-  z e. _V
23 elequ1 
 |-  ( w = z -> ( w e. x <-> z e. x ) )
24 eleq2 
 |-  ( w = z -> ( v e. w <-> v e. z ) )
25 23 24 anbi12d 
 |-  ( w = z -> ( ( w e. x /\ v e. w ) <-> ( z e. x /\ v e. z ) ) )
26 25 exbidv 
 |-  ( w = z -> ( E. v ( w e. x /\ v e. w ) <-> E. v ( z e. x /\ v e. z ) ) )
27 22 26 elab 
 |-  ( z e. { w | E. v ( w e. x /\ v e. w ) } <-> E. v ( z e. x /\ v e. z ) )
28 19.42v 
 |-  ( E. v ( z e. x /\ v e. z ) <-> ( z e. x /\ E. v v e. z ) )
29 n0 
 |-  ( z =/= (/) <-> E. v v e. z )
30 29 anbi2i 
 |-  ( ( z e. x /\ z =/= (/) ) <-> ( z e. x /\ E. v v e. z ) )
31 28 30 bitr4i 
 |-  ( E. v ( z e. x /\ v e. z ) <-> ( z e. x /\ z =/= (/) ) )
32 21 27 31 3bitrri 
 |-  ( ( z e. x /\ z =/= (/) ) <-> z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } )
33 eleq2 
 |-  ( dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( z e. dom f <-> z e. dom { <. w , v >. | ( w e. x /\ v e. w ) } ) )
34 32 33 bitr4id 
 |-  ( dom f = dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) )
35 19 34 syl 
 |-  ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) )
36 35 adantl 
 |-  ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( ( z e. x /\ z =/= (/) ) <-> z e. dom f ) )
37 fnfun 
 |-  ( f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } -> Fun f )
38 funfvima3 
 |-  ( ( Fun f /\ f C_ { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( z e. dom f -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) )
39 38 ancoms 
 |-  ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ Fun f ) -> ( z e. dom f -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) )
40 37 39 sylan2 
 |-  ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( z e. dom f -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) )
41 36 40 sylbid 
 |-  ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( ( z e. x /\ z =/= (/) ) -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) ) )
42 41 imp 
 |-  ( ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) /\ ( z e. x /\ z =/= (/) ) ) -> ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) )
43 imasng 
 |-  ( z e. _V -> ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u } )
44 43 elv 
 |-  ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u }
45 vex 
 |-  u e. _V
46 elequ1 
 |-  ( v = u -> ( v e. z <-> u e. z ) )
47 46 anbi2d 
 |-  ( v = u -> ( ( z e. x /\ v e. z ) <-> ( z e. x /\ u e. z ) ) )
48 eqid 
 |-  { <. w , v >. | ( w e. x /\ v e. w ) } = { <. w , v >. | ( w e. x /\ v e. w ) }
49 22 45 25 47 48 brab 
 |-  ( z { <. w , v >. | ( w e. x /\ v e. w ) } u <-> ( z e. x /\ u e. z ) )
50 49 abbii 
 |-  { u | z { <. w , v >. | ( w e. x /\ v e. w ) } u } = { u | ( z e. x /\ u e. z ) }
51 44 50 eqtri 
 |-  ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = { u | ( z e. x /\ u e. z ) }
52 ibar 
 |-  ( z e. x -> ( u e. z <-> ( z e. x /\ u e. z ) ) )
53 52 abbi2dv 
 |-  ( z e. x -> z = { u | ( z e. x /\ u e. z ) } )
54 51 53 eqtr4id 
 |-  ( z e. x -> ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) = z )
55 54 eleq2d 
 |-  ( z e. x -> ( ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) <-> ( f ` z ) e. z ) )
56 55 ad2antrl 
 |-  ( ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) /\ ( z e. x /\ z =/= (/) ) ) -> ( ( f ` z ) e. ( { <. w , v >. | ( w e. x /\ v e. w ) } " { z } ) <-> ( f ` z ) e. z ) )
57 42 56 mpbid 
 |-  ( ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) /\ ( z e. x /\ z =/= (/) ) ) -> ( f ` z ) e. z )
58 57 exp32 
 |-  ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> ( z e. x -> ( z =/= (/) -> ( f ` z ) e. z ) ) )
59 58 ralrimiv 
 |-  ( ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
60 59 eximi 
 |-  ( E. f ( f C_ { <. w , v >. | ( w e. x /\ v e. w ) } /\ f Fn dom { <. w , v >. | ( w e. x /\ v e. w ) } ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
61 18 60 syl 
 |-  ( A. y E. f ( f C_ y /\ f Fn dom y ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
62 61 alrimiv 
 |-  ( A. y E. f ( f C_ y /\ f Fn dom y ) -> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
63 eqid 
 |-  ( w e. dom y |-> ( f ` { u | w y u } ) ) = ( w e. dom y |-> ( f ` { u | w y u } ) )
64 63 aceq3lem 
 |-  ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. f ( f C_ y /\ f Fn dom y ) )
65 64 alrimiv 
 |-  ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. y E. f ( f C_ y /\ f Fn dom y ) )
66 62 65 impbii 
 |-  ( A. y E. f ( f C_ y /\ f Fn dom y ) <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
67 1 66 bitri 
 |-  ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )