Theorem elo 10444

Description: See eloprabg 4007. 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 2782	. . 3 |- <.<.A, B>., <.C, D>.>. e. V
2		eqeq1 1481	. . . . . . . . . 10 |- (u = <.<.A, B>., <.C, D>.>. -> (u = <.<.y, z>., <.v, w>.>. <-> <.<.A, B>., <.C, D>.>. = <.<.y, z>., <.v, w>.>.))
3		eqcom 1477	. . . . . . . . . 10 |- (<.<.A, B>., <.C, D>.>. = <.<.y, z>., <.v, w>.>. <-> <.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>.)
4	2, 3	syl6bb 536	. . . . . . . . 9 |- (u = <.<.A, B>., <.C, D>.>. -> (u = <.<.y, z>., <.v, w>.>. <-> <.<.y, z>., <.v, w>.>. = <.<.A, B>., <.C, D>.>.))
5		visset 1813	. . . . . . . . . . . . 13 |- y e. V
6		visset 1813	. . . . . . . . . . . . 13 |- z e. V
7		opex 2782	. . . . . . . . . . . . 13 |- <.v, w>. e. V
8	5, 6, 7	otthg 2790	. . . . . . . . . . . 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 799	. . . . . . . . . . 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 1813	. . . . . . . . . . . . . . 15 |- v e. V
11		visset 1813	. . . . . . . . . . . . . . 15 |- w e. V
12	10, 11	opthg 2788	. . . . . . . . . . . . . 14 |- (D e. V -> (<.v, w>. = <.C, D>. <-> (v = C /\ w = D)))
13	12	3anbi3d 899	. . . . . . . . . . . . 13 |- (D e. V -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> (y = A /\ z = B /\ (v = C /\ w = D))))
14		and4as 10432	. . . . . . . . . . . . 13 |- ((y = A /\ z = B /\ (v = C /\ w = D)) <-> ((y = A /\ z = B /\ v = C) /\ w = D))
15	13, 14	syl6bb 536	. . . . . . . . . . . 12 |- (D e. V -> ((y = A /\ z = B /\ <.v, w>. = <.C, D>.) <-> ((y = A /\ z = B /\ v = C) /\ w = D)))
16	15	3ad2ant3 802	. . . . . . . . . . 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 528	. . . . . . . . . 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 789	. . . . . . . . . . 11 |- ((A e. V /\ B e. V /\ C e. V) -> B e. V)
19	18	adantr 389	. . . . . . . . . 10 |- (((A e. V /\ B e. V /\ C e. V) /\ D e. V) -> B e. V)
20		opelxpi 3217	. . . . . . . . . . 11 |- ((C e. V /\ D e. V) -> <.C, D>. e. (V X. V))
21	20	3ad2antl3 811	. . . . . . . . . 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 858	. . . . . . . . 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 541	. . . . . . . 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 617	. . . . . . 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 891	. . . . . . . . 9 |- ((y = A /\ z = B /\ v = C) -> (ph <-> th))
30		elo.4	. . . . . . . . 9 |- (w = D -> (th <-> ta))
31	29, 30	sylan9bb 540	. . . . . . . 8 |- (((y = A /\ z = B /\ v = C) /\ w = D) -> (ph <-> ta))
32	31	pm5.32i 645	. . . . . . 7 |- ((((y = A /\ z = B /\ v = C) /\ w = D) /\ ph) <-> (((y = A /\ z = B /\ v = C) /\ w = D) /\ ta))
33	25, 32	syl6bb 536	. . . . . 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 1283	. . . . 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 1534	. . . . . . 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 1813	. . . . . . . 8 |- u e. V
37		eqeq1 1481	. . . . . . . . . 10 |- (x = u -> (x = <.<.y, z>., <.v, w>.>. <-> u = <.<.y, z>., <.v, w>.>.))
38	37	anbi1d 617	. . . . . . . . 9 |- (x = u -> ((x = <.<.y, z>., <.v, w>.>. /\ ph) <-> (u = <.<.y, z>., <.v, w>.>. /\ ph)))
39	38	4exbidv 1283	. . . . . . . 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 1897	. . . . . . 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 534	. . . . . 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 388	. . . . 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