Metamath Proof Explorer

Theorem dfac5

Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Theorem 6M(4) of Enderton p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC. (Contributed by NM, 11-Apr-2004) (Revised by Mario Carneiro, 17-May-2015)

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

Proof

Step Hyp Ref Expression
1 dfac4 
 |-  ( CHOICE <-> A. x E. f ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) )
2 neeq1 
 |-  ( z = w -> ( z =/= (/) <-> w =/= (/) ) )
3 2 cbvralvw 
 |-  ( A. z e. x z =/= (/) <-> A. w e. x w =/= (/) )
4 3 anbi2i 
 |-  ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) <-> ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. w e. x w =/= (/) ) )
5 r19.26 
 |-  ( A. w e. x ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) <-> ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. w e. x w =/= (/) ) )
6 4 5 bitr4i 
 |-  ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) <-> A. w e. x ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) )
7 pm3.35 
 |-  ( ( w =/= (/) /\ ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( f ` w ) e. w )
8 7 ancoms 
 |-  ( ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) -> ( f ` w ) e. w )
9 8 ralimi 
 |-  ( A. w e. x ( ( w =/= (/) -> ( f ` w ) e. w ) /\ w =/= (/) ) -> A. w e. x ( f ` w ) e. w )
10 6 9 sylbi 
 |-  ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) -> A. w e. x ( f ` w ) e. w )
11 r19.26 
 |-  ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( A. w e. x ( f ` w ) e. w /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) )
12 elin 
 |-  ( v e. ( z i^i ran f ) <-> ( v e. z /\ v e. ran f ) )
13 fvelrnb 
 |-  ( f Fn x -> ( v e. ran f <-> E. t e. x ( f ` t ) = v ) )
14 13 biimpac 
 |-  ( ( v e. ran f /\ f Fn x ) -> E. t e. x ( f ` t ) = v )
15 fveq2 
 |-  ( w = t -> ( f ` w ) = ( f ` t ) )
16 id 
 |-  ( w = t -> w = t )
17 15 16 eleq12d 
 |-  ( w = t -> ( ( f ` w ) e. w <-> ( f ` t ) e. t ) )
18 neeq2 
 |-  ( w = t -> ( z =/= w <-> z =/= t ) )
19 ineq2 
 |-  ( w = t -> ( z i^i w ) = ( z i^i t ) )
20 19 eqeq1d 
 |-  ( w = t -> ( ( z i^i w ) = (/) <-> ( z i^i t ) = (/) ) )
21 18 20 imbi12d 
 |-  ( w = t -> ( ( z =/= w -> ( z i^i w ) = (/) ) <-> ( z =/= t -> ( z i^i t ) = (/) ) ) )
22 17 21 anbi12d 
 |-  ( w = t -> ( ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) ) )
23 22 rspcv 
 |-  ( t e. x -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) ) )
24 minel 
 |-  ( ( ( f ` t ) e. t /\ ( z i^i t ) = (/) ) -> -. ( f ` t ) e. z )
25 24 ex 
 |-  ( ( f ` t ) e. t -> ( ( z i^i t ) = (/) -> -. ( f ` t ) e. z ) )
26 25 imim2d 
 |-  ( ( f ` t ) e. t -> ( ( z =/= t -> ( z i^i t ) = (/) ) -> ( z =/= t -> -. ( f ` t ) e. z ) ) )
27 26 imp 
 |-  ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) -> ( z =/= t -> -. ( f ` t ) e. z ) )
28 27 necon4ad 
 |-  ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) -> ( ( f ` t ) e. z -> z = t ) )
29 eleq1 
 |-  ( ( f ` t ) = v -> ( ( f ` t ) e. z <-> v e. z ) )
30 29 biimpar 
 |-  ( ( ( f ` t ) = v /\ v e. z ) -> ( f ` t ) e. z )
31 28 30 impel 
 |-  ( ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) /\ ( ( f ` t ) = v /\ v e. z ) ) -> z = t )
32 fveq2 
 |-  ( z = t -> ( f ` z ) = ( f ` t ) )
33 eqeq2 
 |-  ( ( f ` t ) = v -> ( ( f ` z ) = ( f ` t ) <-> ( f ` z ) = v ) )
34 eqcom 
 |-  ( ( f ` z ) = v <-> v = ( f ` z ) )
35 33 34 bitrdi 
 |-  ( ( f ` t ) = v -> ( ( f ` z ) = ( f ` t ) <-> v = ( f ` z ) ) )
36 32 35 syl5ib 
 |-  ( ( f ` t ) = v -> ( z = t -> v = ( f ` z ) ) )
37 36 ad2antrl 
 |-  ( ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) /\ ( ( f ` t ) = v /\ v e. z ) ) -> ( z = t -> v = ( f ` z ) ) )
38 31 37 mpd 
 |-  ( ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) /\ ( ( f ` t ) = v /\ v e. z ) ) -> v = ( f ` z ) )
39 38 exp32 
 |-  ( ( ( f ` t ) e. t /\ ( z =/= t -> ( z i^i t ) = (/) ) ) -> ( ( f ` t ) = v -> ( v e. z -> v = ( f ` z ) ) ) )
40 23 39 syl6com 
 |-  ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( t e. x -> ( ( f ` t ) = v -> ( v e. z -> v = ( f ` z ) ) ) ) )
41 40 com14 
 |-  ( v e. z -> ( t e. x -> ( ( f ` t ) = v -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) ) )
42 41 rexlimdv 
 |-  ( v e. z -> ( E. t e. x ( f ` t ) = v -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) )
43 14 42 syl5 
 |-  ( v e. z -> ( ( v e. ran f /\ f Fn x ) -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) )
44 43 expd 
 |-  ( v e. z -> ( v e. ran f -> ( f Fn x -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> v = ( f ` z ) ) ) ) )
45 44 com4t 
 |-  ( f Fn x -> ( A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. z -> ( v e. ran f -> v = ( f ` z ) ) ) ) )
46 45 imp4b 
 |-  ( ( f Fn x /\ A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) ) -> ( ( v e. z /\ v e. ran f ) -> v = ( f ` z ) ) )
47 12 46 syl5bi 
 |-  ( ( f Fn x /\ A. w e. x ( ( f ` w ) e. w /\ ( z =/= w -> ( z i^i w ) = (/) ) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) )
48 11 47 sylan2br 
 |-  ( ( f Fn x /\ ( A. w e. x ( f ` w ) e. w /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) )
49 48 anassrs 
 |-  ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) )
50 49 adantlr 
 |-  ( ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. ( z i^i ran f ) -> v = ( f ` z ) ) )
51 fveq2 
 |-  ( w = z -> ( f ` w ) = ( f ` z ) )
52 id 
 |-  ( w = z -> w = z )
53 51 52 eleq12d 
 |-  ( w = z -> ( ( f ` w ) e. w <-> ( f ` z ) e. z ) )
54 53 rspcv 
 |-  ( z e. x -> ( A. w e. x ( f ` w ) e. w -> ( f ` z ) e. z ) )
55 fnfvelrn 
 |-  ( ( f Fn x /\ z e. x ) -> ( f ` z ) e. ran f )
56 55 expcom 
 |-  ( z e. x -> ( f Fn x -> ( f ` z ) e. ran f ) )
57 54 56 anim12d 
 |-  ( z e. x -> ( ( A. w e. x ( f ` w ) e. w /\ f Fn x ) -> ( ( f ` z ) e. z /\ ( f ` z ) e. ran f ) ) )
58 elin 
 |-  ( ( f ` z ) e. ( z i^i ran f ) <-> ( ( f ` z ) e. z /\ ( f ` z ) e. ran f ) )
59 57 58 syl6ibr 
 |-  ( z e. x -> ( ( A. w e. x ( f ` w ) e. w /\ f Fn x ) -> ( f ` z ) e. ( z i^i ran f ) ) )
60 59 expd 
 |-  ( z e. x -> ( A. w e. x ( f ` w ) e. w -> ( f Fn x -> ( f ` z ) e. ( z i^i ran f ) ) ) )
61 60 com13 
 |-  ( f Fn x -> ( A. w e. x ( f ` w ) e. w -> ( z e. x -> ( f ` z ) e. ( z i^i ran f ) ) ) )
62 61 imp31 
 |-  ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( f ` z ) e. ( z i^i ran f ) )
63 eleq1 
 |-  ( v = ( f ` z ) -> ( v e. ( z i^i ran f ) <-> ( f ` z ) e. ( z i^i ran f ) ) )
64 62 63 syl5ibrcom 
 |-  ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( v = ( f ` z ) -> v e. ( z i^i ran f ) ) )
65 64 adantr 
 |-  ( ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v = ( f ` z ) -> v e. ( z i^i ran f ) ) )
66 50 65 impbid 
 |-  ( ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) /\ A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) )
67 66 ex 
 |-  ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) )
68 67 alrimdv 
 |-  ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) )
69 fvex 
 |-  ( f ` z ) e. _V
70 eqeq2 
 |-  ( h = ( f ` z ) -> ( v = h <-> v = ( f ` z ) ) )
71 70 bibi2d 
 |-  ( h = ( f ` z ) -> ( ( v e. ( z i^i ran f ) <-> v = h ) <-> ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) )
72 71 albidv 
 |-  ( h = ( f ` z ) -> ( A. v ( v e. ( z i^i ran f ) <-> v = h ) <-> A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) ) )
73 69 72 spcev 
 |-  ( A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) -> E. h A. v ( v e. ( z i^i ran f ) <-> v = h ) )
74 eu6 
 |-  ( E! v v e. ( z i^i ran f ) <-> E. h A. v ( v e. ( z i^i ran f ) <-> v = h ) )
75 73 74 sylibr 
 |-  ( A. v ( v e. ( z i^i ran f ) <-> v = ( f ` z ) ) -> E! v v e. ( z i^i ran f ) )
76 68 75 syl6 
 |-  ( ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) /\ z e. x ) -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E! v v e. ( z i^i ran f ) ) )
77 76 ralimdva 
 |-  ( ( f Fn x /\ A. w e. x ( f ` w ) e. w ) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) )
78 77 ex 
 |-  ( f Fn x -> ( A. w e. x ( f ` w ) e. w -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) )
79 10 78 syl5 
 |-  ( f Fn x -> ( ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) /\ A. z e. x z =/= (/) ) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) )
80 79 expd 
 |-  ( f Fn x -> ( A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) -> ( A. z e. x z =/= (/) -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) ) ) )
81 80 imp4b 
 |-  ( ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> A. z e. x E! v v e. ( z i^i ran f ) ) )
82 vex 
 |-  f e. _V
83 82 rnex 
 |-  ran f e. _V
84 ineq2 
 |-  ( y = ran f -> ( z i^i y ) = ( z i^i ran f ) )
85 84 eleq2d 
 |-  ( y = ran f -> ( v e. ( z i^i y ) <-> v e. ( z i^i ran f ) ) )
86 85 eubidv 
 |-  ( y = ran f -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( z i^i ran f ) ) )
87 86 ralbidv 
 |-  ( y = ran f -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x E! v v e. ( z i^i ran f ) ) )
88 83 87 spcev 
 |-  ( A. z e. x E! v v e. ( z i^i ran f ) -> E. y A. z e. x E! v v e. ( z i^i y ) )
89 81 88 syl6 
 |-  ( ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
90 89 exlimiv 
 |-  ( E. f ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
91 90 alimi 
 |-  ( A. x E. f ( f Fn x /\ A. w e. x ( w =/= (/) -> ( f ` w ) e. w ) ) -> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
92 1 91 sylbi 
 |-  ( CHOICE -> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
93 eqid 
 |-  { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
94 eqid 
 |-  ( U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } i^i y ) = ( U. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } i^i y )
95 biid 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
96 93 94 95 dfac5lem5 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
97 96 alrimiv 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> A. h E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
98 dfac3 
 |-  ( CHOICE <-> A. h E. f A. w e. h ( w =/= (/) -> ( f ` w ) e. w ) )
99 97 98 sylibr 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> CHOICE )
100 92 99 impbii 
 |-  ( CHOICE <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )