Theorem aceq5 4712

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is similar to the Axiom of Choice (first form) of [Enderton] p. 49. 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.

Assertion

Ref	Expression
aceq5	|- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))

Distinct variable group:   x,f,z,y,w,v

Proof of Theorem aceq5

Step	Hyp	Ref	Expression
1		aceq4 4706	. . 3 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.xE.f(f Fn x /\ A.w e. x (w =/= (/) -> (f` w) e. w)))
2		fveq2 3709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> (f` w) = (f` t))
3		id 59	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> w = t)
4	2, 3	eleq12d 1534	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = t -> ((f` w) e. w <-> (f` t) e. t))
5		neeq2 1583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> (z =/= w <-> z =/= t))
6		ineq2 2201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = t -> (z i^i w) = (z i^i t))
7	6	eqeq1d 1475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> ((z i^i w) = (/) <-> (z i^i t) = (/)))
8	5, 7	imbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = t -> ((z =/= w -> (z i^i w) = (/)) <-> (z =/= t -> (z i^i t) = (/))))
9	4, 8	anbi12d 626	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = t -> (((f` w) e. w /\ (z =/= w -> (z i^i w) = (/))) <-> ((f` t) e. t /\ (z =/= t -> (z i^i t) = (/)))))
10	9	rcla4v 1864	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (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) = (/)))))
11		minel 2314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((f` t) e. t /\ (z i^i t) = (/)) -> -. (f` t) e. z)
12	11	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` t) e. t -> ((z i^i t) = (/) -> -. (f` t) e. z))
13	12	imim2d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f` t) e. t -> ((z =/= t -> (z i^i t) = (/)) -> (z =/= t -> -. (f` t) e. z)))
14	13	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) -> (z =/= t -> -. (f` t) e. z))
15	14	necon4ad 1618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) -> ((f` t) e. z -> z = t))
16	15	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ (f` t) e. z) -> z = t)
17		eleq1 1526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f` t) = v -> ((f` t) e. z <-> v e. z))
18	17	biimpar 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((f` t) = v /\ v e. z) -> (f` t) e. z)
19	16, 18	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> z = t)
20		eqeq2 1476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` t) = v -> ((f` z) = (f` t) <-> (f` z) = v))
21		eqcom 1469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` z) = v <-> v = (f` z))
22	20, 21	syl6bb 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f` t) = v -> ((f` z) = (f` t) <-> v = (f` z)))
23		fveq2 3709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = t -> (f` z) = (f` t))
24	22, 23	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f` t) = v -> (z = t -> v = (f` z)))
25	24	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> (z = t -> v = (f` z)))
26	19, 25	mpd 26	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> v = (f` z))
27	26	exp32 377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f` t) e. t /\ (z =/= t -> (z i^i t) = (/))) -> ((f` t) = v -> (v e. z -> v = (f` z))))
28	10, 27	syl6com 53	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (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)))))
29	28	com14 38	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (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)))))
30	29	r19.23adv 1738	. . . . . . . . . . . . . . . . . . . . . . 23 |- (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))))
31		fvelrnb 3745	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f Fn x -> (v e. ran f <-> E.t e. x (f` t) = v))
32	31	biimpac 418	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v e. ran f /\ f Fn x) -> E.t e. x (f` t) = v)
33	30, 32	syl5 21	. . . . . . . . . . . . . . . . . . . . . 22 |- (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))))
34	33	exp3a 375	. . . . . . . . . . . . . . . . . . . . 21 |- (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)))))
35	34	com4t 40	. . . . . . . . . . . . . . . . . . . 20 |- (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)))))
36	35	imp4b 365	. . . . . . . . . . . . . . . . . . 19 |- ((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)))
37		elin 2197	. . . . . . . . . . . . . . . . . . 19 |- (v e. (z i^i ran f) <-> (v e. z /\ v e. ran f))
38	36, 37	syl5ib 206	. . . . . . . . . . . . . . . . . 18 |- ((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)))
39		r19.26 1742	. . . . . . . . . . . . . . . . . 18 |- (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) = (/))))
40	38, 39	sylan2br 453	. . . . . . . . . . . . . . . . 17 |- ((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)))
41	40	anassrs 441	. . . . . . . . . . . . . . . 16 |- (((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)))
42	41	adantlr 393	. . . . . . . . . . . . . . 15 |- ((((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)))
43		eleq1 1526	. . . . . . . . . . . . . . . . 17 |- (v = (f` z) -> (v e. (z i^i ran f) <-> (f` z) e. (z i^i ran f)))
44		fveq2 3709	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = z -> (f` w) = (f` z))
45		id 59	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = z -> w = z)
46	44, 45	eleq12d 1534	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = z -> ((f` w) e. w <-> (f` z) e. z))
47	46	rcla4v 1864	. . . . . . . . . . . . . . . . . . . . . 22 |- (z e. x -> (A.w e. x (f` w) e. w -> (f` z) e. z))
48		fnfvelrn 3798	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((f Fn x /\ z e. x) -> (f` z) e. ran f)
49	48	expcom 374	. . . . . . . . . . . . . . . . . . . . . 22 |- (z e. x -> (f Fn x -> (f` z) e. ran f))
50	47, 49	anim12d 556	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. x -> ((A.w e. x (f` w) e. w /\ f Fn x) -> ((f` z) e. z /\ (f` z) e. ran f)))
51		elin 2197	. . . . . . . . . . . . . . . . . . . . 21 |- ((f` z) e. (z i^i ran f) <-> ((f` z) e. z /\ (f` z) e. ran f))
52	50, 51	syl6ibr 213	. . . . . . . . . . . . . . . . . . . 20 |- (z e. x -> ((A.w e. x (f` w) e. w /\ f Fn x) ->