Theorem aceq6b 4666

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 4671). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 4522 and preleq 4527 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 4665.)

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 4657	. 2 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z))
2		hbra1 1663	. . . . . 6 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> A.zA.z e. x (z =/= (/) -> (f` z) e. z))
3		ra4 1670	. . . . . . . . . . . 12 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (z e. x -> (z =/= (/) -> (f` z) e. z)))
4		fvex 3671	. . . . . . . . . . . . . . 15 |- (f` z) e. V
5		eleq1 1510	. . . . . . . . . . . . . . . 16 |- (w = (f` z) -> (w e. z <-> (f` z) e. z))
6		eleq1 1510	. . . . . . . . . . . . . . . . . 18 |- (w = (f` z) -> (w e. v <-> (f` z) e. v))
7	6	anbi2d 614	. . . . . . . . . . . . . . . . 17 |- (w = (f` z) -> ((z e. v /\ w e. v) <-> (z e. v /\ (f` z) e. v)))
8	7	rexbidv 1640	. . . . . . . . . . . . . . . 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 626	. . . . . . . . . . . . . . 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 1842	. . . . . . . . . . . . . 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 1452	. . . . . . . . . . . . . . . . . . 19 |- z = z
12		neeq1 1566	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (u =/= (/) <-> z =/= (/)))
13		eqeq1 1457	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (u = z <-> z = z))
14	12, 13	anbi12d 626	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> ((u =/= (/) /\ u = z) <-> (z =/= (/) /\ z = z)))
15	14	rcla4ev 1850	. . . . . . . . . . . . . . . . . . 19 |- ((z e. x /\ (z =/= (/) /\ z = z)) -> E.u e. x (u =/= (/) /\ u = z))
16	11, 15	mpanr2 707	. . . . . . . . . . . . . . . . . 18 |- ((z e. x /\ z =/= (/)) -> E.u e. x (u =/= (/) /\ u = z))
17		fveq2 3663	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = z -> (f` u) = (f` z))
18		preq1 2418	. . . . . . . . . . . . . . . . . . . . . 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 2419	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> {(f` z), u} = {(f` z), z})
21	19, 20	eqtr2d 1484	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> {(f` z), z} = {(f` u), u})
22	21	anim2i 335	. . . . . . . . . . . . . . . . . . 19 |- ((u =/= (/) /\ u = z) -> (u =/= (/) /\ {(f` z), z} = {(f` u), u}))
23	22	r19.22si 1710	. . . . . . . . . . . . . . . . . 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 2749	. . . . . . . . . . . . . . . . . 18 |- {(f` z), z} e. V
26		eqeq1 1457	. . . . . . . . . . . . . . . . . . . 20 |- (g = {(f` z), z} -> (g = {(f` u), u} <-> {(f` z), z} = {(f` u), u}))
27	26	anbi2d 614	. . . . . . . . . . . . . . . . . . 19 |- (g = {(f` z), z} -> ((u =/= (/) /\ g = {(f` u), u}) <-> (u =/= (/) /\ {(f` z), z} = {(f` u), u})))
28	27	rexbidv 1640	. . . . . . . . . . . . . . . . . 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 1869	. . . . . . . . . . . . . . . . 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 200	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ z =/= (/)) -> {(f` z), z} e. {g | E.u e. x (u =/= (/) /\ g = {(f` u), u})})
31		visset 1788	. . . . . . . . . . . . . . . . . 18 |- z e. V
32	31	pri2 2421	. . . . . . . . . . . . . . . . 17 |- z e. {(f` z), z}
33	4	pri1 2420	. . . . . . . . . . . . . . . . 17 |- (f` z) e. {(f` z), z}
34	32, 33	pm3.2i 285	. . . . . . . . . . . . . . . 16 |- (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})
35	30, 34	jctir 293	. . . . . . . . . . . . . . 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 1511	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> (z e. v <-> z e. {(f` z), z}))
37		eleq2 1511	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> ((f` z) e. v <-> (f` z) e. {(f` z), z}))
38	36, 37	anbi12d 626	. . . . . . . . . . . . . . . 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 1850	. . . . . . . . . . . . . . 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 451	. . . . . . . . . . . . 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 373	. . . . . . . . . . . 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 361	. . . . . . . . . 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 65	. . . . . . . . 9 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> ((z e. x /\ z =/= (/)) -> E.w(