Theorem aceq3lem 4704

Description: Lemma for aceq3 4705.

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 1804	. . . . . 6 |- y e. V
2		rnexg 3345	. . . . . 6 |- (y e. V -> ran y e. V)
3	1, 2	ax-mp 7	. . . . 5 |- ran y e. V
4	3	pwex 2735	. . . 4 |- P~ran y e. V
5		raleq1 1778	. . . . 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	exbidv 1274	. . . 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 1859	. . 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 3256	. . . . . . . . 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	9	releqi 3234	. . . . . . . . 9 |- (Rel F <-> Rel {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
11	8, 10	mpbir 190	. . . . . . . 8 |- Rel F
12	11	a1i 8	. . . . . . 7 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> Rel F)
13	9	eleq2i 1530	. . . . . . . . . . . 12 |- (<.t, h>. e. F <-> <.t, h>. e. {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
14		visset 1804	. . . . . . . . . . . . 13 |- t e. V
15		visset 1804	. . . . . . . . . . . . 13 |- h e. V
16		eleq1 1526	. . . . . . . . . . . . . 14 |- (w = t -> (w e. dom y <-> t e. dom y))
17		breq1 2612	. . . . . . . . . . . . . . . . 17 |- (w = t -> (wyu <-> tyu))
18	17	abbidv 1569	. . . . . . . . . . . . . . . 16 |- (w = t -> {u | wyu} = {u | tyu})
19	18	fveq2d 3713	. . . . . . . . . . . . . . 15 |- (w = t -> (f` {u | wyu}) = (f` {u | tyu}))
20	19	eqeq2d 1478	. . . . . . . . . . . . . 14 |- (w = t -> (v = (f` {u | wyu}) <-> v = (f` {u | tyu})))
21	16, 20	anbi12d 626	. . . . . . . . . . . . 13 |- (w = t -> ((w e. dom y /\ v = (f` {u | wyu})) <-> (t e. dom y /\ v = (f` {u | tyu}))))
22		eqeq1 1473	. . . . . . . . . . . . . 14 |- (v = h -> (v = (f` {u | tyu}) <-> h = (f` {u | tyu})))
23	22	anbi2d 614	. . . . . . . . . . . . 13 |- (v = h -> ((t e. dom y /\ v = (f` {u | tyu})) <-> (t e. dom y /\ h = (f` {u | tyu}))))
24	14, 15, 21, 23	opelopab 2809	. . . . . . . . . . . 12 |- (<.t, h>. e. {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))} <-> (t e. dom y /\ h = (f` {u | tyu})))
25	13, 24	bitr 173	. . . . . . . . . . 11 |- (<.t, h>. e. F <-> (t e. dom y /\ h = (f` {u | tyu})))
26	25	pm3.26bi 322	. . . . . . . . . 10 |- (<.t, h>. e. F -> t e. dom y)
27		19.8a 1025	. . . . . . . . . . . . . . . . 17 |- (tyu -> E.t tyu)
28	27	ss2abi 2110	. . . . . . . . . . . . . . . 16 |- {u | tyu} (_ {u | E.t tyu}
29		dfrn2 3292	. . . . . . . . . . . . . . . 16 |- ran y = {u | E.t tyu}
30	28, 29	sseqtr4 2084	. . . . . . . . . . . . . . 15 |- {u | tyu} (_ ran y
31	3	elpw2 2718	. . . . . . . . . . . . . . 15 |- ({u | tyu} e. P~ran y <-> {u | tyu} (_ ran y)
32	30, 31	mpbir 190	. . . . . . . . . . . . . 14 |- {u | tyu} e. P~ran y
33		neeq1 1582	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> (z =/= (/) <-> {u | tyu} =/= (/)))
34		fveq2 3709	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> (f` z) = (f` {u | tyu}))
35		id 59	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> z = {u | tyu})
36	34, 35	eleq12d 1534	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> ((f` z) e. z <-> (f` {u | tyu}) e. {u | tyu}))
37	33, 36	imbi12d 624	. . . . . . . . . . . . . . 15 |- (z = {u | tyu} -> ((z =/= (/) -> (f` z) e. z) <-> ({u | tyu} =/= (/) -> (f` {u | tyu}) e. {u | tyu})))
38	37	rcla4v 1864	. . . . . . . . . . . . . 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})))
39	32, 38	ax-mp 7	. . . . . . . . . . . . 13 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> ({u | tyu} =/= (/) -> (f` {u | tyu}) e. {u | tyu}))
40	14	eldm 3296	. . . . . . . . . . . . . 14 |- (t e. dom y <-> E.u tyu)
41		abn0 2280	. . . . . . . . . . . . . 14 |- ({u | tyu} =/= (/) <-> E.u tyu)
42	40, 41	bitr4 176	. . . . . . . . . . . . 13 |- (t e. dom y <-> {u | tyu} =/= (/))
43	39, 42	syl5ib 206	. . . . . . . . . . . 12 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> (t e. dom y -> (f` {u | tyu}) e. {u | tyu}))
44	43	com12 11	. . . . . . . . . . 11 |- (t e. dom y -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> (f` {u | tyu}) e. {u | tyu}))
45		fvex 3717	. . . . . . . . . . . . . 14 |- (f` {u | tyu}) e. V
46	19, 9, 45	fvopab4 3765	. . . . . . . . . . . . 13 |- (t e. dom y -> (F` t) = (f` {u | tyu}))
47	46	eleq1d 1532	. . . . . . . . . . . 12 |- (t e. dom y -> ((F` t) e. {u | tyu} <-> (f` {u | tyu}) e. {u | tyu}))
48		fvex 3717	. . . . . . . . . . . . . 14 |- (F` t) e. V
49		breq2 2613	. . . . . . . . . . . . . 14 |- (h = (F` t) -> (tyh <-> ty(F` t)))
50		breq2 2613	. . . . . . . . . . . . . . 15 |- (u = h -> (tyu <-> tyh))
51	50	cbvabv 1900	. . . . . . . . . . . . . 14 |- {u | tyu} = {h | tyh}
52	48, 49, 51	elab2 1892	. . . . . . . . . . . . 13 |- ((F` t) e. {u | tyu} <-> ty(F` t))
53		df-br 2610	. . . . . . . . . . . . 13 |- (ty(F` t) <-> <.t, (F` t)>. e. y)
54	52, 53	bitr2 174	. . . . . . . . . . . 12 |- (<.t, (F` t)>. e. y <-> (F` t) e. {u | tyu})
55	47, 54	syl5bb 530	. . . . . . . . . . 11 |- (t e. dom y -> (<.t, (F` t)>. e. y <-> (f` {u | tyu}) e. {u | tyu}))
56	44, 55	sylibrd 204	. . . . . . . . . 10 |- (t e. dom y -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> <.t, (F` t)>. e. y))
57	26, 56	syl 10	. . . . . . . . 9 |- (<.t, h>. e. F -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> <.t, (F` t)>. e. y))
58		fvex 3717	. . . . . . . . . . . . 13 |- (f` {u | wyu}) e. V
59	58, 9	fnopab2 3604	. . . . . . . . . . . 12 |- F Fn dom y
60		fnfun 3571	. . . . . . . . . . . 12 |- (F Fn dom y -> Fun F)
61	59, 60	ax-mp 7	. . . . . . . . . . 11 |- Fun F
62	15	funopfv 3736	. . . . . . . . . . 11 |- (Fun F -> (<.t, h>. e. F -> (F` t) = h))
63	61, 62	ax-mp 7	. . . . . . . . . 10 |- (<.t, h>. e. F -> (F` t) = h)
64		opeq2 2479	. . . . . . . . . . 11 |- ((F` t) = h -> <.t, (F` t)>. = <.t, h>.)
65	64	eleq1d 1532	. . . . . . . . . 10 |- ((F` t) = h -> (<.t, (F` t)>. e. y <-> <.t, h>. e. y))
66	63, 65	syl 10	. . . . . . . . 9 |- (<.t, h>. e. F -> (<.t, (F` t)>. e. y <-> <.t, h>. e. y))
67	57, 66	sylibd 202	. . . . . . . 8 |- (<.t, h>. e. F -> (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> <.t, h>. e. y))
68	67	com12 11	. . . . . . 7 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> (<.t, h>. e. F -> <.t, h>. e. y))
69	12, 68	relssdv 3239	. . . . . 6 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> F (_ y)