Theorem aceq3lem 4794

Description: Lemma for aceq3 4795.

Hypothesis

Ref	Expression
aceq3lem.1	|- F = {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))}

Assertion

Ref	Expression
aceq3lem	|- (A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z) -> E.f(f (_ y /\ f Fn dom y))

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

Proof of Theorem aceq3lem

Step	Hyp	Ref	Expression
1		visset 1860	. . . . . 6 |- y e. V
2	1	rnex 3418	. . . . 5 |- ran y e. V
3	2	pwex 2801	. . . 4 |- P~ran y e. V
4		raleq1 1833	. . . . 5 |- (x = P~ran y -> (A.z e. x (z =/= (/) -> (f` z) e. z) <-> A.z e. P~ ran y(z =/= (/) -> (f` z) e. z)))
5	4	exbidv 1321	. . . 4 |- (x = P~ran y -> (E.fA.z e. x (z =/= (/) -> (f` z) e. z) <-> E.fA.z e. P~ ran y(z =/= (/) -> (f` z) e. z)))
6	3, 5	cla4v 1915	. . 3 |- (A.xE.fA.z e. x (z =/= (/) -> (f` z) e. z) -> E.fA.z e. P~ ran y(z =/= (/) -> (f` z) e. z))
7		relopab 3323	. . . . . . . . 9 |- Rel {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))}
8		aceq3lem.1	. . . . . . . . . 10 |- F = {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))}
9	8	releqi 3301	. . . . . . . . 9 |- (Rel F <-> Rel {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
10	7, 9	mpbir 197	. . . . . . . 8 |- Rel F
11	10	a1i 8	. . . . . . 7 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> Rel F)
12	8	eleq2i 1585	. . . . . . . . . . . 12 |- (<.t, h>. e. F <-> <.t, h>. e. {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
13		visset 1860	. . . . . . . . . . . . 13 |- t e. V
14		visset 1860	. . . . . . . . . . . . 13 |- h e. V
15		eleq1 1581	. . . . . . . . . . . . . 14 |- (w = t -> (w e. dom y <-> t e. dom y))
16		breq1 2677	. . . . . . . . . . . . . . . . 17 |- (w = t -> (wyu <-> tyu))
17	16	abbidv 1624	. . . . . . . . . . . . . . . 16 |- (w = t -> {u | wyu} = {u | tyu})
18	17	fveq2d 3785	. . . . . . . . . . . . . . 15 |- (w = t -> (f` {u | wyu}) = (f` {u | tyu}))
19	18	eqeq2d 1533	. . . . . . . . . . . . . 14 |- (w = t -> (v = (f` {u | wyu}) <-> v = (f` {u | tyu})))
20	15, 19	anbi12d 639	. . . . . . . . . . . . 13 |- (w = t -> ((w e. dom y /\ v = (f` {u | wyu})) <-> (t e. dom y /\ v = (f` {u | tyu}))))
21		eqeq1 1528	. . . . . . . . . . . . . 14 |- (v = h -> (v = (f` {u | tyu}) <-> h = (f` {u | tyu})))
22	21	anbi2d 627	. . . . . . . . . . . . 13 |- (v = h -> ((t e. dom y /\ v = (f` {u | tyu})) <-> (t e. dom y /\ h = (f` {u | tyu}))))
23	13, 14, 20, 22	opelopab 2876	. . . . . . . . . . . 12 |- (<.t, h>. e. {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))} <-> (t e. dom y /\ h = (f` {u | tyu})))
24	12, 23	bitri 180	. . . . . . . . . . 11 |- (<.t, h>. e. F <-> (t e. dom y /\ h = (f` {u | tyu})))
25	24	pm3.26bi 329	. . . . . . . . . 10 |- (<.t, h>. e. F -> t e. dom y)
26		19.8a 1070	. . . . . . . . . . . . . . . . 17 |- (tyu -> E.t tyu)
27	26	ss2abi 2171	. . . . . . . . . . . . . . . 16 |- {u | tyu} (_ {u | E.t tyu}
28		dfrn2 3360	. . . . . . . . . . . . . . . 16 |- ran y = {u | E.t tyu}
29	27, 28	sseqtr4i 2145	. . . . . . . . . . . . . . 15 |- {u | tyu} (_ ran y
30	2	elpw2 2783	. . . . . . . . . . . . . . 15 |- ({u | tyu} e. P~ran y <-> {u | tyu} (_ ran y)
31	29, 30	mpbir 197	. . . . . . . . . . . . . 14 |- {u | tyu} e. P~ran y
32		neeq1 1637	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> (z =/= (/) <-> {u | tyu} =/= (/)))
33		fveq2 3781	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> (f` z) = (f` {u | tyu}))
34		id 59	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> z = {u | tyu})
35	33, 34	eleq12d 1589	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> ((f` z) e. z <-> (f` {u | tyu}) e. {u | tyu}))
36	32, 35	imbi12d 637	. . . . . . . . . . . . . . 15 |- (z = {u | tyu} -> ((z =/= (/) -> (f` z) e. z) <-> ({u | tyu} =/= (/) -> (f` {u | tyu}) e. {u | tyu})))
37	36	rcla4v 1920	. . . . . . . . . . . . . 14 |- ({u | tyu} e. P~ran y -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> ({u | tyu} =/= (/) -> (f` {u | tyu}) e. {u | tyu})))
38	31, 37	ax-mp 7	. . . . . . . . . . . . 13 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> ({u | tyu} =/= (/) -> (f` {u | tyu}) e. {u | tyu}))
39	13	eldm 3364	. . . . . . . . . . . . . 14 |- (t e. dom y <-> E.u tyu)
40		abn0 2342	. . . . . . . . . . . . . 14 |- ({u | tyu} =/= (/) <-> E.u tyu)
41	39, 40	bitr4i 183	. . . . . . . . . . . . 13 |- (t e. dom y <-> {u | tyu} =/= (/))
42	38, 41	syl5ib 213	. . . . . . . . . . . 12 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> (t e. dom y -> (f` {u | tyu}) e. {u | tyu}))
43	42	com12 11	. . . . . . . . . . 11 |- (t e. dom y -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> (f` {u | tyu}) e. {u | tyu}))
44		fvex 3789	. . . . . . . . . . . . . 14 |- (f` {u | tyu}) e. V
45	18, 8, 44	fvopab4 3837	. . . . . . . . . . . . 13 |- (t e. dom y -> (F` t) = (f` {u | tyu}))
46	45	eleq1d 1587	. . . . . . . . . . . 12 |- (t e. dom y -> ((F` t) e. {u | tyu} <-> (f` {u | tyu}) e. {u | tyu}))
47		fvex 3789	. . . . . . . . . . . . . 14 |- (F` t) e. V
48		breq2 2678	. . . . . . . . . . . . . 14 |- (h = (F` t) -> (tyh <-> ty(F` t)))
49		breq2 2678	. . . . . . . . . . . . . . 15 |- (u = h -> (tyu <-> tyh))
50	49	cbvabv 1956	. . . . . . . . . . . . . 14 |- {u | tyu} = {h | tyh}
51	47, 48, 50	elab2 1948	. . . . . . . . . . . . 13 |- ((F` t) e. {u | tyu} <-> ty(F` t))
52		df-br 2675	. . . . . . . . . . . . 13 |- (ty(F` t) <-> <.t, (F` t)>. e. y)
53	51, 52	bitr2i 181	. . . . . . . . . . . 12 |- (<.t, (F` t)>. e. y <-> (F` t) e. {u | tyu})
54	46, 53	syl5bb 543	. . . . . . . . . . 11 |- (t e. dom y -> (<.t, (F` t)>. e. y <-> (f` {u | tyu}) e. {u | tyu}))
55	43, 54	sylibrd 211	. . . . . . . . . 10 |- (t e. dom y -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> <.t, (F` t)>. e. y))
56	25, 55	syl 10	. . . . . . . . 9 |- (<.t, h>. e. F -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> <.t, (F` t)>. e. y))
57		fvex 3789	. . . . . . . . . . . . 13 |- (f` {u | wyu}) e. V
58	57, 8	fnopab2 3675	. . . . . . . . . . . 12 |- F Fn dom y
59		fnfun 3642	. . . . . . . . . . . 12 |- (F Fn dom y -> Fun F)
60	58, 59	ax-mp 7	. . . . . . . . . . 11 |- Fun F
61	14	funopfv 3808	. . . . . . . . . . 11 |- (Fun F -> (<.t, h>. e. F -> (F` t) = h))
62	60, 61	ax-mp 7	. . . . . . . . . 10 |- (<.t, h>. e. F -> (F` t) = h)
63		opeq2 2542	. . . . . . . . . . 11 |- ((F` t) = h -> <.t, (F` t)>. = <.t, h>.)
64	63	eleq1d 1587	. . . . . . . . . 10 |- ((F` t) = h -> (<.t, (F` t)>. e. y <-> <.t, h>. e. y))
65	62, 64	syl 10	. . . . . . . . 9 |- (<.t, h>. e. F -> (<.t, (F` t)>. e. y <-> <.t, h>. e. y))
66	56, 65	sylibd 209	. . . . . . . 8 |- (<.t, h>. e. F -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> <.t, h>. e. y))
67	66	com12 11	. . . . . . 7 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> (<.t, h>. e. F -> <.t, h>. e. y))
68	11, 67	relssdv 3306	. . . . . 6 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> F (_ y)
69	68, 58	jctir 300	. . . . 5 |- (A.z e. P~ ran y(z