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	imbitrid	\|- ( ( 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	biimtrid	\|- ( ( 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	imbitrrdi	\|- ( 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		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 ) ) )
95		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 )
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 ) ) )

Metamath Proof Explorer

Theorem dfac5

Proof