Theorem aceq3lem 3555

Description: Lemma for aceq3 3556.

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

Proof of Theorem aceq3lem

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 |- y e. V
2		rnexg 2569	. . . . . 6 |- (y e. V -> ran y e. V)
3	1, 2	ax-mp 6	. . . . 5 |- ran y e. V
4	3	pwex 1806	. . . 4 |- P~ran y e. V
5		raleq 1324	. . . . 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)))
6	5	biexdv 936	. . . 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)))
7	4, 6	cla4v 1400	. . 3 |- (A.xE.fA.z e. x (-. z = (/) -> (f` z) e. z) -> E.fA.z e. P~ ran y(-. z = (/) -> (f` z) e. z))
8		relopab 2494	. . . . . . . . 9 |- Rel {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))}
9		aceq3lem.1	. . . . . . . . . 10 |- F = {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))}
10		releq 2477	. . . . . . . . . 10 |- (F = {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))} -> (Rel F <-> Rel {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))}))
11	9, 10	ax-mp 6	. . . . . . . . 9 |- (Rel F <-> Rel {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
12	8, 11	mpbir 165	. . . . . . . 8 |- Rel F
13	12	a1i 7	. . . . . . 7 |- (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> Rel F)
14	9	eleq2i 1153	. . . . . . . . . . . 12 |- (<.t, h>. e. F <-> <.t, h>. e. {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
15		visset 1350	. . . . . . . . . . . . 13 |- t e. V
16		visset 1350	. . . . . . . . . . . . 13 |- h e. V
17		eleq1 1149	. . . . . . . . . . . . . 14 |- (w = t -> (w e. dom y <-> t e. dom y))
18		breq1 2065	. . . . . . . . . . . . . . . . 17 |- (w = t -> (wyu <-> tyu))
19	18	biabdv 1183	. . . . . . . . . . . . . . . 16 |- (w = t -> {u | wyu} = {u | tyu})
20	19	fveq2d 2836	. . . . . . . . . . . . . . 15 |- (w = t -> (f` {u | wyu}) = (f` {u | tyu}))
21	20	cleq2d 1112	. . . . . . . . . . . . . 14 |- (w = t -> (v = (f` {u | wyu}) <-> v = (f` {u | tyu})))
22	17, 21	anbi12d 476	. . . . . . . . . . . . 13 |- (w = t -> ((w e. dom y /\ v = (f` {u | wyu})) <-> (t e. dom y /\ v = (f` {u | tyu}))))
23		cleq1 1107	. . . . . . . . . . . . . 14 |- (v = h -> (v = (f` {u | tyu}) <-> h = (f` {u | tyu})))
24	23	anbi2d 468	. . . . . . . . . . . . 13 |- (v = h -> ((t e. dom y /\ v = (f` {u | tyu})) <-> (t e. dom y /\ h = (f` {u | tyu}))))
25	15, 16, 22, 24	opelopab 2117	. . . . . . . . . . . 12 |- (<.t, h>. e. {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))} <-> (t e. dom y /\ h = (f` {u | tyu})))
26	14, 25	bitr 151	. . . . . . . . . . 11 |- (<.t, h>. e. F <-> (t e. dom y /\ h = (f` {u | tyu})))
27	26	pm3.26bd 259	. . . . . . . . . 10 |- (<.t, h>. e. F -> t e. dom y)
28		19.8a 712	. . . . . . . . . . . . . . . . 17 |- (tyu -> E.t tyu)
29	28	ss2abi 1552	. . . . . . . . . . . . . . . 16 |- {u | tyu} (_ {u | E.t tyu}
30		dfrn2 2523	. . . . . . . . . . . . . . . 16 |- ran y = {u | E.t tyu}
31	29, 30	sseqtr4 1533	. . . . . . . . . . . . . . 15 |- {u | tyu} (_ ran y
32		elpw2g 1803	. . . . . . . . . . . . . . . 16 |- (ran y e. V -> ({u | tyu} e. P~ran y <-> {u | tyu} (_ ran y))
33	3, 32	ax-mp 6	. . . . . . . . . . . . . . 15 |- ({u | tyu} e. P~ran y <-> {u | tyu} (_ ran y)
34	31, 33	mpbir 165	. . . . . . . . . . . . . 14 |- {u | tyu} e. P~ran y
35		cleq1 1107	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> (z = (/) <-> {u | tyu} = (/)))
36	35	negbid 463	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> (-. z = (/) <-> -. {u | tyu} = (/)))
37		fveq2 2832	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> (f` z) = (f` {u | tyu}))
38		id 9	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> z = {u | tyu})
39	37, 38	eleq12d 1157	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> ((f` z) e. z <-> (f` {u | tyu}) e. {u | tyu}))
40	36, 39	imbi12d 474	. . . . . . . . . . . . . . 15 |- (z = {u | tyu} -> ((-. z = (/) -> (f` z) e. z) <-> (-. {u | tyu} = (/) -> (f` {u | tyu}) e. {u | tyu})))
41	40	rcla4v 1402	. . . . . . . . . . . . . 14 |- (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> ({u | tyu} e. P~ran y -> (-. {u | tyu} = (/) -> (f` {u | tyu}) e. {u | tyu})))
42	34, 41	mpi 44	. . . . . . . . . . . . 13 |- (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> (-. {u | tyu} = (/) -> (f` {u | tyu}) e. {u | tyu}))
43	15	eldm 2527	. . . . . . . . . . . . . 14 |- (t e. dom y <-> E.u tyu)
44		abn0 1715	. . . . . . . . . . . . . 14 |- (-. {u | tyu} = (/) <-> E.u tyu)
45	43, 44	bitr4 154	. . . . . . . . . . . . 13 |- (t e. dom y <-> -. {u | tyu} = (/))
46	42, 45	syl5ib 181	. . . . . . . . . . . 12 |- (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> (t e. dom y -> (f` {u | tyu}) e. {u | tyu}))
47	46	com12 13	. . . . . . . . . . 11 |- (t e. dom y -> (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> (f` {u | tyu}) e. {u | tyu}))
48		fvex 2838	. . . . . . . . . . . . . 14 |- (f` {u | tyu}) e. V
49	20, 9, 48	fvopab4 2871	. . . . . . . . . . . . 13 |- (t e. dom y -> (F` t) = (f` {u | tyu}))
50	49	eleq1d 1155	. . . . . . . . . . . 12 |- (t e. dom y -> ((F` t) e. {u | tyu} <-> (f` {u | tyu}) e. {u | tyu}))
51		fvex 2838	. . . . . . . . . . . . . 14 |- (F` t) e. V
52		breq2 2066	. . . . . . . . . . . . . 14 |- (h = (F` t) -> (tyh <-> ty(F` t)))
53		breq2 2066	. . . . . . . . . . . . . . 15 |- (u = h -> (tyu <-> tyh))
54	53	cbvabv 1424	. . . . . . . . . . . . . 14 |- {u | tyu} = {h | tyh}
55	51, 52, 54	elab2 1419	. . . . . . . . . . . . 13 |- ((F` t) e. {u | tyu} <-> ty(F` t))
56		df-br 2063	. . . . . . . . . . . . 13 |- (ty(F` t) <-> <.t, (F` t)>. e. y)
57	55, 56	bitr2 152	. . . . . . . . . . . 12 |- (<.t, (F` t)>. e. y <-> (F` t) e. {u | tyu})
58	50, 57	syl5bb 410	. . . . . . . . . . 11 |- (t e. dom y -> (<.t, (F` t)>. e. y <-> (f` {u | tyu}) e. {u | tyu}))
59	47, 58	sylibrd 179	. . . . . . . . . 10 |- (t e. dom y -> (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> <.t, (F` t)>. e. y))
60	27, 59	syl 12	. . . . . . . . 9 |- (<.t, h>. e. F -> (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> <.t, (F` t)>. e. y))
61		fvex 2838	. . . . . . . . . . . . 13 |- (f` {u | wyu}) e. V
62	61, 9	fnopab2 2747	. . . . . . . . . . . 12 |- F Fn dom y
63		fnfun 2721	. . . . . . . . . . . 12 |- (F Fn dom y -> Fun F)
64	62, 63	ax-mp 6	. . . . . . . . . . 11 |- Fun F
65	16	funfvopi 2853	. . . . . . . . . . 11 |- (Fun F -> (<.t, h>. e. F -> (F` t) = h))
66	64, 65	ax-mp 6	. . . . . . . . . 10 |- (<.t, h>. e. F -> (F` t) = h)
67		opeq2 1877	. . . . . . . . . . 11 |- ((F` t) = h -> <.t, (F` t)>. = <.t, h>.)
68	67	eleq1d 1155	. . . . . . . . . 10 |- ((F` t) = h -> (<.t, (F` t)>. e. y <-> <.t, h>. e. y))
69	66, 68	syl 12	. . . . . . . . 9 |- (<.t, h>. e. F -> (<.t, (F` t)>. e. y <-> <.t, h>. e. y))
70	60, 69	sylibd 177	. . . . . . . 8 |- (<.t, h>. e. F -> (A.z e. P~ ran y(-. z = (/) -> (f` z) e. z) -> <.