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