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