Theorem aceq5lem4 3561

Description: Lemma for aceq5 3563.

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 group(s):   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 1153	. . . 4 |- (z e. A <-> z e. {u | (-. u = (/) /\ E.t e. h u = ({t} X. t))})
3		visset 1350	. . . . . 6 |- z e. V
4		cleq1 1107	. . . . . . . 8 |- (u = z -> (u = (/) <-> z = (/)))
5	4	negbid 463	. . . . . . 7 |- (u = z -> (-. u = (/) <-> -. z = (/)))
6		cleq1 1107	. . . . . . . 8 |- (u = z -> (u = ({t} X. t) <-> z = ({t} X. t)))
7	6	birexdv 1220	. . . . . . 7 |- (u = z -> (E.t e. h u = ({t} X. t) <-> E.t e. h z = ({t} X. t)))
8	5, 7	anbi12d 476	. . . . . 6 |- (u = z -> ((-. u = (/) /\ E.t e. h u = ({t} X. t)) <-> (-. z = (/) /\ E.t e. h z = ({t} X. t))))
9	3, 8	elab 1415	. . . . 5 |- (z e. {u | (-. u = (/) /\ E.t e. h u = ({t} X. t))} <-> (-. z = (/) /\ E.t e. h z = ({t} X. t)))
10	9	pm3.26bd 259	. . . 4 |- (z e. {u | (-. u = (/) /\ E.t e. h u = ({t} X. t))} -> -. z = (/))
11	2, 10	sylbi 174	. . 3 |- (z e. A -> -. z = (/))
12	11	rgen 1247	. 2 |- A.z e. A -. z = (/)
13		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 |- (z = ({t} X. t) -> (x e. z <-> x e. ({t} X. t)))
14		elxp 2442	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. ({t} X. t) <-> E.uE.v(x = <.u, v>. /\ (u e. {t} /\ v e. t)))
15		excom 728	. . . . . . . . . . . . . . . . . . . . 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)))
16	14, 15	bitr 151	. . . . . . . . . . . . . . . . . . . 20 |- (x e. ({t} X. t) <-> E.vE.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)))
17	13, 16	syl6bb 414	. . . . . . . . . . . . . . . . . . 19 |- (z = ({t} X. t) -> (x e. z <-> E.vE.u(x = <.u, v>. /\ (u e. {t} /\ v e. t))))
18		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 |- (w = ({g} X. g) -> (x e. w <-> x e. ({g} X. g)))
19		elxp 2442	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. ({g} X. g) <-> E.uE.y(x = <.u, y>. /\ (u e. {g} /\ y e. g)))
20		excom 728	. . . . . . . . . . . . . . . . . . . . 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)))
21	19, 20	bitr 151	. . . . . . . . . . . . . . . . . . . 20 |- (x e. ({g} X. g) <-> E.yE.u(x = <.u, y>. /\ (u e. {g} /\ y e. g)))
22	18, 21	syl6bb 414	. . . . . . . . . . . . . . . . . . 19 |- (w = ({g} X. g) -> (x e. w <-> E.yE.u(x = <.u, y>. /\ (u e. {g} /\ y e. g))))
23	17, 22	bi2anan9 478	. . . . . . . . . . . . . . . . . 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)))))
24		eeanv 980	. . . . . . . . . . . . . . . . . 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))))
25	23, 24	syl6bbr 416	. . . . . . . . . . . . . . . . 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)))))
26		opeq1 1876	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u = t -> <.u, v>. = <.t, v>.)
27	26	cleq2d 1112	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = t -> (x = <.u, v>. <-> x = <.t, v>.))
28	27	biimpac 326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x = <.u, v>. /\ u = t) -> x = <.t, v>.)
29		elsn 1820	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. {t} <-> u = t)
30	28, 29	sylan2b 347	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x = <.u, v>. /\ u e. {t}) -> x = <.t, v>.)
31	30	adantrr 312	. . . . . . . . . . . . . . . . . . . . 21 |- ((x = <.u, v>. /\ (u e. {t} /\ v e. t)) -> x = <.t, v>.)
32	31	19.23aiv 952	. . . . . . . . . . . . . . . . . . . 20 |- (E.u(x = <.u, v>. /\ (u e. {t} /\ v e. t)) -> x = <.t, v>.)
33		opeq1 1876	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u = g -> <.u, y>. = <.g, y>.)
34	33	cleq2d 1112	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (u = g -> (x = <.u, y>. <-> x = <.g, y>.))
35	34	biimpac 326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x = <.u, y>. /\ u = g) -> x = <.g, y>.)
36		elsn 1820	. . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. {g} <-> u = g)
37	35, 36	sylan2b 347	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x = <.u, y>. /\ u e. {g}) -> x = <.g, y>.)
38	37	adantrr 312	. . . . . . . . . . . . . . . . . . . . 21 |- ((x = <.u, y>. /\ (u e. {g} /\ y e. g)) -> x = <.g, y>.)
39	38	19.23aiv 952	. . . . . . . . . . . . . . . . . . . 20 |- (E.u(x = <.u, y>. /\ (u e. {g} /\ y e. g)) -> x = <.g, y>.)
40	32, 39	anim12i 268	. . . . . . . . . . . . . . . . . . 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>.))
41		cleqtr 1118	. . . . . . . . . . . . . . . . . . . 20 |- ((<.t, v>. = x /\ x = <.g, y>.) -> <.t, v>. = <.g, y>.)
42		cleqcom 1103	. . . . . . . . . . . . . . . . . . . 20 |- (x = <.t, v>. <-> <.t, v>. = x)
43	41, 42	sylanb 344	. . . . . . . . . . . . . . . . . . 19 |- ((x = <.t, v>. /\ x = <.g, y>.) -> <.t, v>. = <.g, y>.)
44		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 |- t e. V
45		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 |- v e. V
46		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 |- y e. V
47	44, 45, 46	opth 1898	. . . . . . . . . . . . . . . . . . . 20 |- (<.t, v>. = <.g, y>. <-> (t = g /\ v = y))
48	47	pm3.26bd 259	. . . . . . . . . . . . . . . . . . 19 |- (<.t, v>. = <.g, y>. -> t = g)
49	40, 43, 48	3syl 21	. . . . . . . . . . . . . . . . . 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)
50	49	19.23aivv 953	. . . . . . . . . . . . . . . . 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)
51	25, 50	syl6bi 187	. . . . . . . . . . . . . . . 16 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> ((x e. z /\ x e. w) -> t = g))
52		sneq 1816	. . . . . . . . . . . . . . . . . 18 |- (t = g -> {t} = {g})
53		xpeq1 2440	. . . . . . . . . . . . . . . . . 18 |- ({t} = {g} -> ({t} X. t) = ({g} X. t))
54	52, 53	syl 12	. . . . . . . . . . . . . . . . 17 |- (t = g -> ({t} X. t) = ({g} X. t))
55		xpeq2 2441	. . . . . . . . . . . . . . . . 17 |- (t = g -> ({g} X. t) = ({g} X. g))
56	54, 55	eqtrd 1128	. . . . . . . . . . . . . . . 16 |- (t = g -> ({t} X. t) = ({g} X. g))
57	51, 56	syl6 23	. . . . . . . . . . . . . . 15 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> ((x e. z /\ x e. w) -> ({t} X. t) = ({g} X. g)))
58		cleq12 1113	. . . . . . . . . . . . . . 15 |- ((z = ({t} X. t) /\ w = ({g} X. g)) -> (z = w <-> ({t} X. t) = ({g} X. g))