Theorem aceq3lem 4732

Description: Lemma for aceq3 4733.

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 1813	. . . . . 6 |- y e. V
2	1	rnex 3361	. . . . 5 |- ran y e. V
3	2	pwex 2745	. . . 4 |- P~ran y e. V
4		raleq1 1786	. . . . 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 1279	. . . 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 1868	. . 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 3266	. . . . . . . . 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 3244	. . . . . . . . 9 |- (Rel F <-> Rel {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
10	7, 9	mpbir 190	. . . . . . . 8 |- Rel F
11	10	a1i 8	. . . . . . 7 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> Rel F)
12	8	eleq2i 1538	. . . . . . . . . . . 12 |- (<.t, h>. e. F <-> <.t, h>. e. {<.w, v>. | (w e. dom y /\ v = (f` {u | wyu}))})
13		visset 1813	. . . . . . . . . . . . 13 |- t e. V
14		visset 1813	. . . . . . . . . . . . 13 |- h e. V
15		eleq1 1534	. . . . . . . . . . . . . 14 |- (w = t -> (w e. dom y <-> t e. dom y))
16		breq1 2622	. . . . . . . . . . . . . . . . 17 |- (w = t -> (wyu <-> tyu))
17	16	abbidv 1577	. . . . . . . . . . . . . . . 16 |- (w = t -> {u | wyu} = {u | tyu})
18	17	fveq2d 3728	. . . . . . . . . . . . . . 15 |- (w = t -> (f` {u | wyu}) = (f` {u | tyu}))
19	18	eqeq2d 1486	. . . . . . . . . . . . . 14 |- (w = t -> (v = (f` {u | wyu}) <-> v = (f` {u | tyu})))
20	15, 19	anbi12d 628	. . . . . . . . . . . . 13 |- (w = t -> ((w e. dom y /\ v = (f` {u | wyu})) <-> (t e. dom y /\ v = (f` {u | tyu}))))
21		eqeq1 1481	. . . . . . . . . . . . . 14 |- (v = h -> (v = (f` {u | tyu}) <-> h = (f` {u | tyu})))
22	21	anbi2d 616	. . . . . . . . . . . . 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 2820	. . . . . . . . . . . 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	bitr 173	. . . . . . . . . . 11 |- (<.t, h>. e. F <-> (t e. dom y /\ h = (f` {u | tyu})))
25	24	pm3.26bi 322	. . . . . . . . . 10 |- (<.t, h>. e. F -> t e. dom y)
26		19.8a 1029	. . . . . . . . . . . . . . . . 17 |- (tyu -> E.t tyu)
27	26	ss2abi 2120	. . . . . . . . . . . . . . . 16 |- {u | tyu} (_ {u | E.t tyu}
28		dfrn2 3303	. . . . . . . . . . . . . . . 16 |- ran y = {u | E.t tyu}
29	27, 28	sseqtr4 2094	. . . . . . . . . . . . . . 15 |- {u | tyu} (_ ran y
30	2	elpw2 2728	. . . . . . . . . . . . . . 15 |- ({u | tyu} e. P~ran y <-> {u | tyu} (_ ran y)
31	29, 30	mpbir 190	. . . . . . . . . . . . . 14 |- {u | tyu} e. P~ran y
32		neeq1 1590	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> (z =/= (/) <-> {u | tyu} =/= (/)))
33		fveq2 3724	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> (f` z) = (f` {u | tyu}))
34		id 59	. . . . . . . . . . . . . . . . 17 |- (z = {u | tyu} -> z = {u | tyu})
35	33, 34	eleq12d 1542	. . . . . . . . . . . . . . . 16 |- (z = {u | tyu} -> ((f` z) e. z <-> (f` {u | tyu}) e. {u | tyu}))
36	32, 35	imbi12d 626	. . . . . . . . . . . . . . 15 |- (z = {u | tyu} -> ((z =/= (/) -> (f` z) e. z) <-> ({u | tyu} =/= (/) -> (f` {u | tyu}) e. {u | tyu})))
37	36	rcla4v 1873	. . . . . . . . . . . . . 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 3307	. . . . . . . . . . . . . 14 |- (t e. dom y <-> E.u tyu)
40		abn0 2290	. . . . . . . . . . . . . 14 |- ({u | tyu} =/= (/) <-> E.u tyu)
41	39, 40	bitr4 176	. . . . . . . . . . . . 13 |- (t e. dom y <-> {u | tyu} =/= (/))
42	38, 41	syl5ib 206	. . . . . . . . . . . 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 3732	. . . . . . . . . . . . . 14 |- (f` {u | tyu}) e. V
45	18, 8, 44	fvopab4 3780	. . . . . . . . . . . . 13 |- (t e. dom y -> (F` t) = (f` {u | tyu}))
46	45	eleq1d 1540	. . . . . . . . . . . 12 |- (t e. dom y -> ((F` t) e. {u | tyu} <-> (f` {u | tyu}) e. {u | tyu}))
47		fvex 3732	. . . . . . . . . . . . . 14 |- (F` t) e. V
48		breq2 2623	. . . . . . . . . . . . . 14 |- (h = (F` t) -> (tyh <-> ty(F` t)))
49		breq2 2623	. . . . . . . . . . . . . . 15 |- (u = h -> (tyu <-> tyh))
50	49	cbvabv 1909	. . . . . . . . . . . . . 14 |- {u | tyu} = {h | tyh}
51	47, 48, 50	elab2 1901	. . . . . . . . . . . . 13 |- ((F` t) e. {u | tyu} <-> ty(F` t))
52		df-br 2620	. . . . . . . . . . . . 13 |- (ty(F` t) <-> <.t, (F` t)>. e. y)
53	51, 52	bitr2 174	. . . . . . . . . . . 12 |- (<.t, (F` t)>. e. y <-> (F` t) e. {u | tyu})
54	46, 53	syl5bb 532	. . . . . . . . . . 11 |- (t e. dom y -> (<.t, (F` t)>. e. y <-> (f` {u | tyu}) e. {u | tyu}))
55	43, 54	sylibrd 204	. . . . . . . . . 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 3732	. . . . . . . . . . . . 13 |- (f` {u | wyu}) e. V
58	57, 8	fnopab2 3618	. . . . . . . . . . . 12 |- F Fn dom y
59		fnfun 3585	. . . . . . . . . . . 12 |- (F Fn dom y -> Fun F)
60	58, 59	ax-mp 7	. . . . . . . . . . 11 |- Fun F
61	14	funopfv 3751	. . . . . . . . . . 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 2488	. . . . . . . . . . 11 |- ((F` t) = h -> <.t, (F` t)>. = <.t, h>.)
64	63	eleq1d 1540	. . . . . . . . . 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 202	. . . . . . . 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 3249	. . . . . 6 |- (A.z e. P~ ran y(z =/= (/) -> (f` z) e. z) -> F (_ y)
69	68, 58	jctir 293	. . . . 5 |- (A.z e. P~ ran y(z