Theorem aceq5 3563

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(s):   x,f,z,y,w,v

Proof of Theorem aceq5

Step	Hyp	Ref	Expression
1		aceq4 3557	. . 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 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> (f` w) = (f` t))
3		id 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> w = t)
4	2, 3	eleq12d 1157	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = t -> ((f` w) e. w <-> (f` t) e. t))
5		cleq2 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = t -> (z = w <-> z = t))
6	5	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> (-. z = w <-> -. z = t))
7		ineq2 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = t -> (z i^i w) = (z i^i t))
8	7	cleq1d 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = t -> ((z i^i w) = (/) <-> (z i^i t) = (/)))
9	6, 8	imbi12d 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = t -> ((-. z = w -> (z i^i w) = (/)) <-> (-. z = t -> (z i^i t) = (/))))
10	4, 9	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = t -> (((f` w) e. w /\ (-. z = w -> (z i^i w) = (/))) <-> ((f` t) e. t /\ (-. z = t -> (z i^i t) = (/)))))
11	10	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.w e. x ((f` w) e. w /\ (-. z = w -> (z i^i w) = (/))) -> (t e. x -> ((f` t) e. t /\ (-. z = t -> (z i^i t) = (/)))))
12		disj 1733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((z i^i t) = (/) <-> A.v e. z -. v e. t)
13		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (v = (f` t) -> (v e. t <-> (f` t) e. t))
14	13	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (v = (f` t) -> (-. v e. t <-> -. (f` t) e. t))
15	14	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (A.v e. z -. v e. t -> ((f` t) e. z -> -. (f` t) e. t))
16	12, 15	sylbi 174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((z i^i t) = (/) -> ((f` t) e. z -> -. (f` t) e. t))
17	16	con2d 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((z i^i t) = (/) -> ((f` t) e. t -> -. (f` t) e. z))
18	17	com12 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((f` t) e. t -> ((z i^i t) = (/) -> -. (f` t) e. z))
19	18	syl3d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((f` t) e. t -> ((-. z = t -> (z i^i t) = (/)) -> (-. z = t -> -. (f` t) e. z)))
20	19	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((f` t) e. t /\ (-. z = t -> (z i^i t) = (/))) -> (-. z = t -> -. (f` t) e. z))
21	20	a3d 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((f` t) e. t /\ (-. z = t -> (z i^i t) = (/))) -> ((f` t) e. z -> z = t))
22	21	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((f` t) e. t /\ (-. z = t -> (z i^i t) = (/))) /\ (f` t) e. z) -> z = t)
23		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f` t) = v -> ((f` t) e. z <-> v e. z))
24	23	biimpar 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((f` t) = v /\ v e. z) -> (f` t) e. z)
25	22, 24	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((f` t) e. t /\ (-. z = t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> z = t)
26		cleq2 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` t) = v -> ((f` z) = (f` t) <-> (f` z) = v))
27		cleqcom 1103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((f` z) = v <-> v = (f` z))
28	26, 27	syl6bb 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((f` t) = v -> ((f` z) = (f` t) <-> v = (f` z)))
29		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (z = t -> (f` z) = (f` t))
30	28, 29	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f` t) = v -> (z = t -> v = (f` z)))
31	30	ad2antrl 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((f` t) e. t /\ (-. z = t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> (z = t -> v = (f` z)))
32	25, 31	mpd 46	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((f` t) e. t /\ (-. z = t -> (z i^i t) = (/))) /\ ((f` t) = v /\ v e. z)) -> v = (f` z))
33	32	exp32 294	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((f` t) e. t /\ (-. z = t -> (z i^i t) = (/))) -> ((f` t) = v -> (v e. z -> v = (f` z))))
34	11, 33	syl6 23	. . . . . . . . . . . . . . . . . . . . . . . . 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)))))
35	34	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)))))
36	35	r19.23adv 1286	. . . . . . . . . . . . . . . . . . . . . . 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))))
37		fvelrn 2883	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (f Fn x -> (v e. ran f <-> E.t e. x (f` t) = v))
38	37	biimpac 326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((v e. ran f /\ f Fn x) -> E.t e. x (f` t) = v)
39	36, 38	syl5 22	. . . . . . . . . . . . . . . . . . . . . 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))))
40	39	exp3a 292	. . . . . . . . . . . . . . . . . . . . 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)))))
41	40	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)))))
42	41	imp4b 283	. . . . . . . . . . . . . . . . . . 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)))
43		elin 1635	. . . . . . . . . . . . . . . . . . 19 |- (v e. (z i^i ran f) <-> (v e. z /\ v e. ran f))
44	42, 43	syl5ib 181	. . . . . . . . . . . . . . . . . 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)))
45		r19.26 1289	. . . . . . . . . . . . . . . . . 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) = (/))))
46	44, 45	sylan2br 348	. . . . . . . . . . . . . . . . 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)))
47	46	anassrs 338	. . . . . . . . . . . . . . . 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)))
48	47	adantlr 310	. . . . . . . . . . . . . . 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)))
49		eleq1 1149	. . . . . . . . . . . . . . . . . 18 |- (v = (f` z) -> (v e. (z i^i ran f) <-> (f` z) e. (z i^i ran f)))
50		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = z -> (f` w) = (f` z))
51		id 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = z -> w = z)
52	50, 51	eleq12d 1157	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = z -> ((f` w) e. w <-> (f` z) e. z))
53	52	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.w e. x (f` w) e. w -> (z e. x -> (f` z) e. z))
54	53	com12 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. x -> (A.w e. x (f` w