Theorem aceq6b 4714

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

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 4705	. 2 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z))
2		hbra1 1679	. . . . . 6 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> A.zA.z e. x (z =/= (/) -> (f` z) e. z))
3		ra4 1686	. . . . . . . . . . . 12 |- (A.z e. x (z =/= (/) -> (f` z) e. z) -> (z e. x -> (z =/= (/) -> (f` z) e. z)))
4		fvex 3717	. . . . . . . . . . . . . . 15 |- (f` z) e. V
5		eleq1 1526	. . . . . . . . . . . . . . . 16 |- (w = (f` z) -> (w e. z <-> (f` z) e. z))
6		eleq1 1526	. . . . . . . . . . . . . . . . . 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 1656	. . . . . . . . . . . . . . . 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 1860	. . . . . . . . . . . . . 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 1468	. . . . . . . . . . . . . . . . . . 19 |- z = z
12		neeq1 1582	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (u =/= (/) <-> z =/= (/)))
13		eqeq1 1473	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (u = z <-> z = z))
14	12, 13	anbi12d 626	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> ((u =/= (/) /\ u = z) <-> (z =/= (/) /\ z = z)))
15	14	rcla4ev 1868	. . . . . . . . . . . . . . . . . . 19 |- ((z e. x /\ (z =/= (/) /\ z = z)) -> E.u e. x (u =/= (/) /\ u = z))
16	11, 15	mpanr2 708	. . . . . . . . . . . . . . . . . 18 |- ((z e. x /\ z =/= (/)) -> E.u e. x (u =/= (/) /\ u = z))
17		fveq2 3709	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = z -> (f` u) = (f` z))
18		preq1 2438	. . . . . . . . . . . . . . . . . . . . . 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 2439	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> {(f` z), u} = {(f` z), z})
21	19, 20	eqtr2d 1500	. . . . . . . . . . . . . . . . . . . 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 1726	. . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . . 18 |- {(f` z), z} e. V
26		eqeq1 1473	. . . . . . . . . . . . . . . . . . . 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 1656	. . . . . . . . . . . . . . . . . 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 1888	. . . . . . . . . . . . . . . . 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 1804	. . . . . . . . . . . . . . . . . 18 |- z e. V
32	31	pri2 2442	. . . . . . . . . . . . . . . . 17 |- z e. {(f` z), z}
33	4	pri1 2441	. . . . . . . . . . . . . . . . 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 1527	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> (z e. v <-> z e. {(f` z), z}))
37		eleq2 1527	. . . . . . . . . . . . . . . . 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 1868	. . . . . . . . . . . . . . 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(w e. z