Theorem aceq5lem4 4800

Description: Lemma for aceq5 4802.

Hypotheses

Ref	Expression
aceq5lem.1	|- A = {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))}
aceq5lem.2	|- B = (U.A i^i y)
aceq5lem.3	|- (ph <-> A.x((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y)))

Assertion

Ref	Expression
aceq5lem4	|- (ph -> E.yA.z e. A E!v v e. (z i^i y))

Distinct variable groups:   x,z,y,w,v,u,t,h   z,B,w   x,A,y,z,w

Proof of Theorem aceq5lem4

Step	Hyp	Ref	Expression
1		aceq5lem.1	. . . . 5 |- A = {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))}
2	1	eleq2i 1585	. . . 4 |- (z e. A <-> z e. {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))})
3		visset 1860	. . . . . 6 |- z e. V
4		neeq1 1637	. . . . . . 7 |- (u = z -> (u =/= (/) <-> z =/= (/)))
5		eqeq1 1528	. . . . . . . 8 |- (u = z -> (u = ({t} X. t) <-> z = ({t} X. t)))
6	5	rexbidv 1711	. . . . . . 7 |- (u = z -> (E.t e. h u = ({t} X. t) <-> E.t e. h z = ({t} X. t)))
7	4, 6	anbi12d 639	. . . . . 6 |- (u = z -> ((u =/= (/) /\ E.t e. h u = ({t} X. t)) <-> (z =/= (/) /\ E.t e. h z = ({t} X. t))))
8	3, 7	elab 1944	. . . . 5 |- (z e. {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))} <-> (z =/= (/) /\ E.t e. h z = ({t} X. t)))
9	8	pm3.26bi 329	. . . 4 |- (z e. {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))} -> z =/= (/))
10	2, 9	sylbi 206	. . 3 |- (z e. A -> z =/= (/))
11	10	rgen 1745	. 2 |- A.z e. A z =/= (/)
12		eleq2 1582	. . . . . . . . . . . . . . . . . . . 20 |- (z = ({t} X. t) -> (x e. z <-> x e. ({t} X. t)))
13		elxp 3259	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. ({t} X. t) <-> E.uE.v(x = <.u, v>. /\ (u e. {t} /\ v e. t)))
14		excom 1087	. . . . . . . . . . . . . . . . . . . . 21 |- (E.uE.v(x = <.u, v>. /\ (u e. {t} /\ v e. t)) <-> E.vE.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)))
15	13, 14	bitri 180	. . . . . . . . . . . . . . . . . . . 20 |- (x e. ({t} X. t) <-> E.vE.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)))
16	12, 15	syl6bb 547	. . . . . . . . . . . . . . . . . . 19 |- (z = ({t} X. t) -> (x e. z <-> E.vE.u(x = <.u, v>. /\ (u e. {t} /\ v e. t))))
17		eleq2 1582	. . . . . . . . . . . . . . . . . . . 20 |- (w = ({g} X. g) -> (x e. w <-> x e. ({g} X. g)))
18		elxp 3259	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. ({g} X. g) <-> E.uE.y(x = <.u, y>. /\ (u e. {g} /\ y e. g)))
19		excom 1087	. . . . . . . . . . . . . . . . . . . . 21 |- (E.uE.y(x = <.u, y>. /\ (u e. {g} /\ y e. g)) <-> E.yE.u(x = <.u, y>. /\ (u e. {g} /\ y e. g)))
20	18, 19	bitri 180	. . . . . . . . . . . . . . . . . . . 20 |- (x e. ({g} X. g) <-> E.yE.u(x = <.u, y>. /\ (u e. {g} /\ y e. g)))
21	17, 20	syl6bb 547	. . . . . . . . . . . . . . . . . . 19 |- (w = ({g} X. g) -> (x e. w <-> E.yE.u(x = <.u, y>. /\ (u e. {g} /\ y e. g))))
22	16, 21	bi2anan9 643	. . . . . . . . . . . . . . . . . 18 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> ((x e. z /\ x e. w) <-> (E.vE.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) /\ E.yE.u(x = <.u, y>. /\ (u e. {g} /\ y e. g)))))
23		eeanv 1365	. . . . . . . . . . . . . . . . . 18 |- (E.vE.y(E.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) /\ E.u(x = <.u, y>. /\ (u e. {g} /\ y e. g))) <-> (E.vE.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) /\ E.yE.u(x = <.u, y>. /\ (u e. {g} /\ y e. g))))
24	22, 23	syl6bbr 549	. . . . . . . . . . . . . . . . 17 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> ((x e. z /\ x e. w) <-> E.vE.y(E.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) /\ E.u(x = <.u, y>. /\ (u e. {g} /\ y e. g)))))
25		opeq1 2541	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u = t -> <.u, v>. = <.t, v>.)
26	25	eqeq2d 1533	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = t -> (x = <.u, v>. <-> x = <.t, v>.))
27	26	biimpac 427	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x = <.u, v>. /\ u = t) -> x = <.t, v>.)
28		elsn 2473	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. {t} <-> u = t)
29	27, 28	sylan2b 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x = <.u, v>. /\ u e. {t}) -> x = <.t, v>.)
30	29	adantrr 404	. . . . . . . . . . . . . . . . . . . . 21 |- ((x = <.u, v>. /\ (u e. {t} /\ v e. t)) -> x = <.t, v>.)
31	30	19.23aiv 1337	. . . . . . . . . . . . . . . . . . . 20 |- (E.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) -> x = <.t, v>.)
32		opeq1 2541	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u = g -> <.u, y>. = <.g, y>.)
33	32	eqeq2d 1533	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = g -> (x = <.u, y>. <-> x = <.g, y>.))
34	33	biimpac 427	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x = <.u, y>. /\ u = g) -> x = <.g, y>.)
35		elsn 2473	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. {g} <-> u = g)
36	34, 35	sylan2b 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x = <.u, y>. /\ u e. {g}) -> x = <.g, y>.)
37	36	adantrr 404	. . . . . . . . . . . . . . . . . . . . 21 |- ((x = <.u, y>. /\ (u e. {g} /\ y e. g)) -> x = <.g, y>.)
38	37	19.23aiv 1337	. . . . . . . . . . . . . . . . . . . 20 |- (E.u(x = <.u, y>. /\ (u e. {g} /\ y e. g)) -> x = <.g, y>.)
39	31, 38	anim12i 340	. . . . . . . . . . . . . . . . . . 19 |- ((E.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) /\ E.u(x = <.u, y>. /\ (u e. {g} /\ y e. g))) -> (x = <.t, v>. /\ x = <.g, y>.))
40		eqtr2 1540	. . . . . . . . . . . . . . . . . . 19 |- ((x = <.t, v>. /\ x = <.g, y>.) -> <.t, v>. = <.g, y>.)
41		visset 1860	. . . . . . . . . . . . . . . . . . . . 21 |- t e. V
42		visset 1860	. . . . . . . . . . . . . . . . . . . . 21 |- v e. V
43		visset 1860	. . . . . . . . . . . . . . . . . . . . 21 |- y e. V
44	41, 42, 43	opth 2843	. . . . . . . . . . . . . . . . . . . 20 |- (<.t, v>. = <.g, y>. <-> (t = g /\ v = y))
45	44	pm3.26bi 329	. . . . . . . . . . . . . . . . . . 19 |- (<.t, v>. = <.g, y>. -> t = g)
46	39, 40, 45	3syl 20	. . . . . . . . . . . . . . . . . 18 |- ((E.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) /\ E.u(x = <.u, y>. /\ (u e. {g} /\ y e. g))) -> t = g)
47	46	19.23aivv 1338	. . . . . . . . . . . . . . . . 17 |- (E.vE.y(E.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) /\ E.u(x = <.u, y>. /\ (u e. {g} /\ y e. g))) -> t = g)
48	24, 47	syl6bi 221	. . . . . . . . . . . . . . . 16 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> ((x e. z /\ x e. w) -> t = g))
49		sneq 2469	. . . . . . . . . . . . . . . . . 18 |- (t = g -> {t} = {g})
50		xpeq1 3257	. . . . . . . . . . . . . . . . . 18 |- ({t} = {g} -> ({t} X. t) = ({g} X. t))
51	49, 50	syl 10	. . . . . . . . . . . . . . . . 17 |- (t = g -> ({t} X. t) = ({g} X. t))
52		xpeq2 3258	. . . . . . . . . . . . . . . . 17 |- (t = g -> ({g} X. t) = ({g} X. g))
53	51, 52	eqtrd 1554	. . . . . . . . . . . . . . . 16 |- (t = g -> ({t} X. t) = ({g} X. g))
54	48, 53	syl6 22	. . . . . . . . . . . . . . 15 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> ((x e. z /\ x e. w) -> ({t} X. t) = ({g} X. g)))
55		eqeq12 1534	. . . . . . . . . . . . . . 15 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> (z = w <-> ({t} X. t) = ({g} X. g)))
56	54, 55	sylibrd 211	. . . . . . . . . . . . . 14 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> ((x e. z /\ x