Theorem elo 10439

Description: See eloprabg 4013. Note: to be used with categories.

Hypotheses

Ref	Expression
elo.1	|- (y = A -> (ph <-> ps))
elo.2	|- (z = B -> (ps <-> ch))
elo.3	|- (v = C -> (ch <-> th))
elo.4	|- (w = D -> (th <-> ta))

Assertion

Ref	Expression
elo	|- (((A e. Q /\ B e. R /\ C e. S) /\ D e. T) -> (<.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> ta))

Distinct variable groups:   v,A,w,y,z   v,B,w,y,z   v,C,w,y,z   v,D,w,y,z   ph,x   ta,v,w,y,z   x,v,w,y,z

Proof of Theorem elo

Step	Hyp	Ref	Expression
1		opex 2788	. . 3 |- <.<.A, B>., <.C, D>.>. e. V
2		eqeq1 1484	. . . . . . . . . 10 |- (u = <.<.A, B>., <.C, D>.>. -> (u = <.<.y, z>., <.v, w>.>. <-> <.<.A, B>., <.C, D>.>. = <.<.y, z>., <.v, w>.>.))
3		eqcom 1480	. . . . . . . . . 10 |- (<.<.A, B>., <.C, D>.>. = <.<.y, z>., <.v, w>.>. <-> <.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>.)
4	2, 3	syl6bb 538	. . . . . . . . 9 |- (u = <.<.A, B>., <.C, D>.>. -> (u = <.<.y, z>., <.v, w>.>. <-> <.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>.))
5		visset 1816	. . . . . . . . . . . . 13 |- y e. V
6		visset 1816	. . . . . . . . . . . . 13 |- z e. V
7		opex 2788	. . . . . . . . . . . . 13 |- <.v, w>. e. V
8	5, 6, 7	otthg 2796	. . . . . . . . . . . 12 |- ((B e. V /\ <.C, D>. e. (V X. V)) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> (y = A /\ z = B /\ <.v, w>. = <.C, D>.)))
9	8	3adant3 801	. . . . . . . . . . 11 |- ((B e. V /\ <.C, D>. e. (V X. V) /\ D e. V) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> (y = A /\ z = B /\ <.v, w>. = <.C, D>.)))
10		visset 1816	. . . . . . . . . . . . . . 15 |- v e. V
11		visset 1816	. . . . . . . . . . . . . . 15 |- w e. V
12	10, 11	opthg 2794	. . . . . . . . . . . . . 14 |- (D e. V -> (<.v, w>. = <.C, D>. <-> (v = C /\ w = D)))
13	12	3anbi3d 901	. . . . . . . . . . . . 13 |- (D e. V -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> (y = A /\ z = B /\ (v = C /\ w = D))))
14		and4as 10427	. . . . . . . . . . . . 13 |- ((y = A /\ z = B /\ (v = C /\ w = D)) <-> ((y = A /\ z = B /\ v = C) /\ w = D))
15	13, 14	syl6bb 538	. . . . . . . . . . . 12 |- (D e. V -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
16	15	3ad2ant3 804	. . . . . . . . . . 11 |- ((B e. V /\ <.C, D>. e. (V X. V) /\ D e. V) -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
17	9, 16	bitrd 530	. . . . . . . . . 10 |- ((B e. V /\ <.C, D>. e. (V X. V) /\ D e. V) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
18		3simp2 791	. . . . . . . . . . 11 |- ((A e. V /\ B e. V /\ C e. V) -> B e. V)
19	18	adantr 391	. . . . . . . . . 10 |- (((A e. V /\ B e. V /\ C e. V) /\ D e. V) -> B e. V)
20		opelxpi 3223	. . . . . . . . . . 11 |- ((C e. V /\ D e. V) -> <.C, D>. e. (V X. V))
21	20	3ad2antl3 813	. . . . . . . . . 10 |- (((A e. V /\ B e. V /\ C e. V) /\ D e. V) -> <.C, D>. e. (V X. V))
22		pm3.27 323	. . . . . . . . . 10 |- (((A e. V /\ B e. V /\ C e. V) /\ D e. V) -> D e. V)
23	17, 19, 21, 22	syl3anc 860	. . . . . . . . 9 |- (((A e. V /\ B e. V /\ C e. V) /\ D e. V) -> (<.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>. <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
24	4, 23	sylan9bbr 543	. . . . . . . 8 |- ((((A e. V /\ B e. V /\ C e. V) /\ D e. V) /\ u = <.<.A, B>., <.C, D>.>.) -> (u = <.<.y, z>., <.v, w>.>. <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
25	24	anbi1d 619	. . . . . . 7 |- ((((A e. V /\ B e. V /\ C e. V) /\ D e. V) /\ u = <.<.A, B>., <.C, D>.>.) -> ((u = <.<.y, z>., <.v, w>.>. /\ ph) <-> (((y = A /\ z = B /\ v = C) /\ w = D) /\ ph)))
26		elo.1	. . . . . . . . . 10 |- (y = A -> (ph <-> ps))
27		elo.2	. . . . . . . . . 10 |- (z = B -> (ps <-> ch))
28		elo.3	. . . . . . . . . 10 |- (v = C -> (ch <-> th))
29	26, 27, 28	syl3an9b 893	. . . . . . . . 9 |- ((y = A /\ z = B /\ v = C) -> (ph <-> th))
30		elo.4	. . . . . . . . 9 |- (w = D -> (th <-> ta))
31	29, 30	sylan9bb 542	. . . . . . . 8 |- (((y = A /\ z = B /\ v = C) /\ w = D) -> (ph <-> ta))
32	31	pm5.32i 647	. . . . . . 7 |- ((((y = A /\ z = B /\ v = C) /\ w = D) /\ ph) <-> (((y = A /\ z = B /\ v = C) /\ w = D) /\ ta))
33	25, 32	syl6bb 538	. . . . . 6 |- ((((A e. V /\ B e. V /\ C e. V) /\ D e. V) /\ u = <.<.A, B>., <.C, D>.>.) -> ((u = <.<.y, z>., <.v, w>.>. /\ ph) <-> (((y = A /\ z = B /\ v = C) /\ w = D) /\ ta)))
34	33	4exbidv 1285	. . . . 5 |- ((((A e. V /\ B e. V /\ C e. V) /\ D e. V) /\ u = <.<.A, B>., <.C, D>.>.) -> (E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph) <-> E.yE.zE.vE.w(((y = A /\ z = B /\ v = C) /\ w = D) /\ ta)))
35		eleq1 1537	. . . . . . 7 |- (u = <.<.A, B>., <.C, D>.>. -> (u e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> <.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)}))
36		visset 1816	. . . . . . . 8 |- u e. V
37		eqeq1 1484	. . . . . . . . . 10 |- (x = u -> (x = <.<.y, z>., <.v, w>.>. <-> u = <.<.y, z>., <.v, w>.>.))
38	37	anbi1d 619	. . . . . . . . 9 |- (x = u -> ((x = <.<.y, z>., <.v, w>.>. /\ ph) <-> (u = <.<.y, z>., <.v, w>.>. /\ ph)))
39	38	4exbidv 1285	. . . . . . . 8 |- (x = u -> (E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph) <-> E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph)))
40	36, 39	elab 1900	. . . . . . 7 |- (u e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)} <-> E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph))
41	35, 40	syl5bbr 536	. . . . . 6 |- (u = <.<.A, B>., <.C, D>.>. -> (E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph) <-> <.<.A, B>., <.C, D>.>. e. {x | E.yE.zE.vE.w(x = <.<.y, z>., <.v, w>.>. /\ ph)}))
42	41	adantl 390	. . . . 5 |- ((((A e. V /\ B e. V /\ C e. V) /\ D e. V) /\ u = <.<.A, B>., <.C, D>.>.) -> (E.yE.zE.vE.w(u = <.<.y, z>., <.v, w>.>. /\ ph) <-> <.<.A, B>., <.C, D>.>. e. {x | E.y