Theorem aceq6b 3565

Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 3568). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, eirrv 3449 and preleq 3454 that are referenced in the proof each make use of Regularity for their derivations. (The reverse derivation can be done without using Regularity; see aceq6a 3564.)

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

Proof of Theorem aceq6b

Step	Hyp	Ref	Expression
1		aceq3 3556	. 2 |- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.xE.fA.z e. x (-. z = (/) -> (f` z) e. z))
2		hbra1 1237	. . . . . 6 |- (A.z e. x (-. z = (/) -> (f` z) e. z) -> A.zA.z e. x (-. z = (/) -> (f` z) e. z))
3		ra4 1243	. . . . . . . . . . . 12 |- (A.z e. x (-. z = (/) -> (f` z) e. z) -> (z e. x -> (-. z = (/) -> (f` z) e. z)))
4		fvex 2838	. . . . . . . . . . . . . . 15 |- (f` z) e. V
5		eleq1 1149	. . . . . . . . . . . . . . . 16 |- (w = (f` z) -> (w e. z <-> (f` z) e. z))
6		eleq1 1149	. . . . . . . . . . . . . . . . . 18 |- (w = (f` z) -> (w e. v <-> (f` z) e. v))
7	6	anbi2d 468	. . . . . . . . . . . . . . . . 17 |- (w = (f` z) -> ((z e. v /\ w e. v) <-> (z e. v /\ (f` z) e. v)))
8	7	birexdv 1220	. . . . . . . . . . . . . . . 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 476	. . . . . . . . . . . . . . 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 1401	. . . . . . . . . . . . . 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		cleqid 1102	. . . . . . . . . . . . . . . . . . 19 |- z = z
12		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = z -> (u = (/) <-> z = (/)))
13	12	negbid 463	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (-. u = (/) <-> -. z = (/)))
14		cleq1 1107	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> (u = z <-> z = z))
15	13, 14	anbi12d 476	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> ((-. u = (/) /\ u = z) <-> (-. z = (/) /\ z = z)))
16	15	rcla4ev 1403	. . . . . . . . . . . . . . . . . . 19 |- ((z e. x /\ (-. z = (/) /\ z = z)) -> E.u e. x (-. u = (/) /\ u = z))
17	11, 16	mpan22 532	. . . . . . . . . . . . . . . . . 18 |- ((z e. x /\ -. z = (/)) -> E.u e. x (-. u = (/) /\ u = z))
18		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . 22 |- (u = z -> (f` u) = (f` z))
19		preq1 1870	. . . . . . . . . . . . . . . . . . . . . 22 |- ((f` u) = (f` z) -> {(f` u), u} = {(f` z), u})
20	18, 19	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> {(f` u), u} = {(f` z), u})
21		preq2 1871	. . . . . . . . . . . . . . . . . . . . 21 |- (u = z -> {(f` z), u} = {(f` z), z})
22	20, 21	eqtr2d 1129	. . . . . . . . . . . . . . . . . . . 20 |- (u = z -> {(f` z), z} = {(f` u), u})
23	22	anim2i 270	. . . . . . . . . . . . . . . . . . 19 |- ((-. u = (/) /\ u = z) -> (-. u = (/) /\ {(f` z), z} = {(f` u), u}))
24	23	r19.22si 1275	. . . . . . . . . . . . . . . . . 18 |- (E.u e. x (-. u = (/) /\ u = z) -> E.u e. x (-. u = (/) /\ {(f` z), z} = {(f` u), u}))
25	17, 24	syl 12	. . . . . . . . . . . . . . . . 17 |- ((z e. x /\ -. z = (/)) -> E.u e. x (-. u = (/) /\ {(f` z), z} = {(f` u), u}))
26		prex 1892	. . . . . . . . . . . . . . . . . 18 |- {(f` z), z} e. V
27		cleq1 1107	. . . . . . . . . . . . . . . . . . . 20 |- (g = {(f` z), z} -> (g = {(f` u), u} <-> {(f` z), z} = {(f` u), u}))
28	27	anbi2d 468	. . . . . . . . . . . . . . . . . . 19 |- (g = {(f` z), z} -> ((-. u = (/) /\ g = {(f` u), u}) <-> (-. u = (/) /\ {(f` z), z} = {(f` u), u})))
29	28	birexdv 1220	. . . . . . . . . . . . . . . . . 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})))
30	26, 29	elab 1415	. . . . . . . . . . . . . . . . 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}))
31	25, 30	sylibr 175	. . . . . . . . . . . . . . . 16 |- ((z e. x /\ -. z = (/)) -> {(f` z), z} e. {g | E.u e. x (-. u = (/) /\ g = {(f` u), u})})
32		visset 1350	. . . . . . . . . . . . . . . . . 18 |- z e. V
33	32	pri2 1842	. . . . . . . . . . . . . . . . 17 |- z e. {(f` z), z}
34	4	pri1 1841	. . . . . . . . . . . . . . . . 17 |- (f` z) e. {(f` z), z}
35	33, 34	pm3.2i 234	. . . . . . . . . . . . . . . 16 |- (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})
36	31, 35	jctir 241	. . . . . . . . . . . . . . 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})))
37		eleq2 1150	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> (z e. v <-> z e. {(f` z), z}))
38		eleq2 1150	. . . . . . . . . . . . . . . . 17 |- (v = {(f` z), z} -> ((f` z) e. v <-> (f` z) e. {(f` z), z}))
39	37, 38	anbi12d 476	. . . . . . . . . . . . . . . 16 |- (v = {(f` z), z} -> ((z e. v /\ (f` z) e. v) <-> (z e. {(f` z), z} /\ (f` z) e. {(f` z), z})))
40	39	rcla4ev 1403	. . . . . . . . . . . . . . 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))
41	36, 40	syl 12	. . . . . . . . . . . . . 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))
42	10, 41	sylan2 346	. . . . . . . . . . . . 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)))
43	42	exp 291	. . . . . . . . . . . 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))))
44	3, 43	syl8 25	. . . . . . . . . . 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))))))
45	44	imp3a 279	. . . . . . . . . 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)))))
46	45	pm2.43d 59	. . . . . . . . 9 |- (A.z e. x (-. z = (/) -> (f` z) e. z)