Theorem aceq6b 4804

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 4809). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 4658 and preleq 4665 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see aceq6a 4803.)

Assertion

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

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

Proof of Theorem aceq6b

Step	Hyp	Ref	Expression
1		aceq3 4795	. 2 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z))
2		hbra1 1734	. . . . . 6 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> A.zA.z e. x (z =/= (/) -> (f` z) e. z))
3		ra4 1741	. . . . . . . . . . . 12 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (z e. x -> (z =/= (/) -> (f` z) e. z)))
4		fvex 3789	. . . . . . . . . . . . . . 15 |- (f` z) e. V
5		eleq1 1581	. . . . . . . . . . . . . . . 16 |- (w = (f` z) -> (w e. z <-> (f` z) e. z))
6		eleq1 1581	. . . . . . . . . . . . . . . . . 18 |- (w = (f` z) -> (w e. v <-> (f` z) e. v))
7	6	anbi2d 627	. . . . . . . . . . . . . . . . 17 |- (w = (f` z) -> ((z e. v /\ w e. v) <-> (z e. v /\ (f` z) e. v)))
8	7	rexbidv 1711	. . . . . . . . . . . . . . . 16 |- (w = (f` z) -> (E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v) <-> E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v)))
9	5, 8	anbi12d 639	. . . . . . . . . . . . . . 15 |- (w = (f` z) -> ((w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)) <-> ((f` z) e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v))))
10	4, 9	cla4ev 1916	. . . . . . . . . . . . . 14 |- (((f` z) e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
11		eqid 1522	. . . . . . . . . . . . . . . . . . 19 |- z = z
12		neeq1 1637	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (u =/= (/) <-> z =/= (/)))
13		eqeq1 1528	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (u = z <-> z = z))
14	12, 13	anbi12d 639	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> ((u =/= (/) /\ u = z) <-> (z =/= (/) /\ z = z)))
15	14	rcla4ev 1924	. . . . . . . . . . . . . . . . . . 19 |- ((z e. x /\ (z =/= (/) /\ z = z)) -> E.u e. x (u =/= (/) /\ u = z))
16	11, 15	mpanr2 722	. . . . . . . . . . . . . . . . . 18 |- ((z e. x /\ z =/= (/)) -> E.u e. x (u =/= (/) /\ u = z))
17		fveq2 3781	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = z -> (f` u) = (f` z))
18		preq1 2500	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` u) = (f` z) -> {(f` u), u} = {(f` z), u})
19	17, 18	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> {(f` u), u} = {(f` z), u})
20		preq2 2501	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> {(f` z), u} = {(f` z), z})
21	19, 20	eqtr2d 1555	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> {(f` z), z} = {(f` u), u})
22	21	anim2i 342	. . . . . . . . . . . . . . . . . . 19 |- ((u =/= (/) /\ u = z) -> (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
23	22	r19.22si 1781	. . . . . . . . . . . . . . . . . 18 |- (E.u e. x (u =/= (/) /\ u = z) -> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
24	16, 23	syl 10	. . . . . . . . . . . . . . . . 17 |- ((z e. x /\ z =/= (/)) -> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
25		prex 2837	. . . . . . . . . . . . . . . . . 18 |- {(f` z), z} e. V
26		eqeq1 1528	. . . . . . . . . . . . . . . . . . . 20 |- (g = {(f` z), z} -> (g = {(f` u), u} <-> {(f` z), z} = {(f` u), u}))
27	26	anbi2d 627	. . . . . . . . . . . . . . . . . . 19 |- (g = {(f` z), z} -> ((u =/= (/) /\ g = {(f` u), u}) <-> (u =/= (/) /\ {(f` z), z} = {(f` u), u})))
28	27	rexbidv 1711	. . . . . . . . . . . . . . . . . 18 |- (g = {(f` z), z} -> (E.u e. x (u =/= (/) /\ g = {(f` u), u}) <-> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u})))
29	25, 28	elab 1944	. . . . . . . . . . . . . . . . 17 |- ({(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} <-> E.u e. x (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
30	24, 29	sylibr 207	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ z =/= (/)) -> {(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})})
31		visset 1860	. . . . . . . . . . . . . . . . . 18 |- z e. V
32	31	prid2 2505	. . . . . . . . . . . . . . . . 17 |- z e. {(f` z), z}
33	4	prid1 2504	. . . . . . . . . . . . . . . . 17 |- (f` z) e. {(f` z), z}
34	32, 33	pm3.2i 292	. . . . . . . . . . . . . . . 16 |- (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})
35	30, 34	jctir 300	. . . . . . . . . . . . . . 15 |- ((z e. x /\ z =/= (/)) -> ({(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} /\ (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})))
36		eleq2 1582	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> (z e. v <-> z e. {(f` z), z}))
37		eleq2 1582	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> ((f` z) e. v <-> (f` z) e. {(f` z), z}))
38	36, 37	anbi12d 639	. . . . . . . . . . . . . . . 16 |- (v = {(f` z), z} -> ((z e. v /\ (f` z) e. v) <-> (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})))
39	38	rcla4ev 1924	. . . . . . . . . . . . . . 15 |- (({(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} /\ (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})) -> E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v))
40	35, 39	syl 10	. . . . . . . . . . . . . 14 |- ((z e. x /\ z =/= (/)) -> E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ (f` z) e. v))
41	10, 40	sylan2 462	. . . . . . . . . . . . 13 |- (((f` z) e. z /\ (z e. x /\ z =/= (/))) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))
42	41	ex 380	. . . . . . . . . . . 12 |- ((f` z) e. z -> ((z e. x /\ z =/= (/)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))
43	3, 42	syl8 24	. . . . . . . . . . 11 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (z e. x -> (z =/= (/) -> ((z e. x /\ z =/= (/)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v))))))
44	43	imp3a 368	. . . . . . . . . 10 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. x /\ z =/= (/)) -> ((z e. x /\ z =/= (/)) -> E.w(w e. z /\ E.v e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})} (z e. v /\ w e. v)))))
45	44	pm2.43d 66	. . . . . . . . 9 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. x /\ z =/= (/)) -> E.w(w