Theorem brecop 5365

Description: Binary relation on a quotient set. Lemma for real number construction.

Hypotheses

Ref	Expression
brecop.1	|- S e. _V
brecop.2	|- Er S
brecop.3	|- dom S = (G X. G)
brecop.4	|- H = ((G X. G)/.S)
brecop.5	|- R = {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))}
brecop.6	|- ((((z e. G /\ w e. G) /\ (A e. G /\ B e. G)) /\ ((v e. G /\ u e. G) /\ (C e. G /\ D e. G))) -> (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (ph <-> ps)))

Assertion

Ref	Expression
brecop	|- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ([<.A, B>.]SR[<.C, D>.]S <-> ps))

Distinct variable groups:   x,y,z,w,v,u,A   x,B,y,z,w,v,u   x,C,y,z,w,v,u   x,D,y,z,w,v,u   x,S,y,z,w,v,u   x,H,y   z,G,w,v,u   ph,x,y   ps,z,w,v,u

Proof of Theorem brecop

Step	Hyp	Ref	Expression
1		eleq1 1957	. . . . . . . 8 |- (x = [<.A, B>.]S -> (x e. H <-> [<.A, B>.]S e. H))
2	1	anbi1d 679	. . . . . . 7 |- (x = [<.A, B>.]S -> ((x e. H /\ y e. H) <-> ([<.A, B>.]S e. H /\ y e. H)))
3		eqeq1 1890	. . . . . . . . . 10 |- (x = [<.A, B>.]S -> (x = [<.z, w>.]S <-> [<.A, B>.]S = [<.z, w>.]S))
4	3	anbi1d 679	. . . . . . . . 9 |- (x = [<.A, B>.]S -> ((x = [<.z, w>.]S /\ y = [<.v, u>.]S) <-> ([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S)))
5	4	anbi1d 679	. . . . . . . 8 |- (x = [<.A, B>.]S -> (((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> (([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)))
6	5	4exbidv 1661	. . . . . . 7 |- (x = [<.A, B>.]S -> (E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)))
7	2, 6	anbi12d 690	. . . . . 6 |- (x = [<.A, B>.]S -> (((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)) <-> (([<.A, B>.]S e. H /\ y e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))))
8		eleq1 1957	. . . . . . . 8 |- (y = [<.C, D>.]S -> (y e. H <-> [<.C, D>.]S e. H))
9	8	anbi2d 678	. . . . . . 7 |- (y = [<.C, D>.]S -> (([<.A, B>.]S e. H /\ y e. H) <-> ([<.A, B>.]S e. H /\ [<.C, D>.]S e. H)))
10		eqeq1 1890	. . . . . . . . . 10 |- (y = [<.C, D>.]S -> (y = [<.v, u>.]S <-> [<.C, D>.]S = [<.v, u>.]S))
11	10	anbi2d 678	. . . . . . . . 9 |- (y = [<.C, D>.]S -> (([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) <-> ([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S)))
12	11	anbi1d 679	. . . . . . . 8 |- (y = [<.C, D>.]S -> ((([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> (([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
13	12	4exbidv 1661	. . . . . . 7 |- (y = [<.C, D>.]S -> (E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph) <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
14	9, 13	anbi12d 690	. . . . . 6 |- (y = [<.C, D>.]S -> ((([<.A, B>.]S e. H /\ y e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph)) <-> (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph))))
15	7, 14	opelopabg 3567	. . . . 5 |- (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) -> (<.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))} <-> (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) /\ E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph))))
16	15	bianabs 715	. . . 4 |- (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) -> (<.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))} <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
17		df-br 3339	. . . . 5 |- ([<.A, B>.]SR[<.C, D>.]S <-> <.[<.A, B>.]S, [<.C, D>.]S>. e. R)
18		brecop.5	. . . . . 6 |- R = {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))}
19	18	eleq2i 1961	. . . . 5 |- (<.[<.A, B>.]S, [<.C, D>.]S>. e. R <-> <.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))})
20	17, 19	bitri 190	. . . 4 |- ([<.A, B>.]SR[<.C, D>.]S <-> <.[<.A, B>.]S, [<.C, D>.]S>. e. {<.x, y>. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [<.z, w>.]S /\ y = [<.v, u>.]S) /\ ph))})
21	16, 20	syl5bb 591	. . 3 |- (([<.A, B>.]S e. H /\ [<.C, D>.]S e. H) -> ([<.A, B>.]SR[<.C, D>.]S <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
22		brecop.1	. . . 4 |- S e. _V
23		brecop.4	. . . 4 |- H = ((G X. G)/.S)
24	22, 23	ecopqsi 5351	. . 3 |- ((A e. G /\ B e. G) -> [<.A, B>.]S e. H)
25	22, 23	ecopqsi 5351	. . 3 |- ((C e. G /\ D e. G) -> [<.C, D>.]S e. H)
26	21, 24, 25	syl2an 503	. 2 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ([<.A, B>.]SR[<.C, D>.]S <-> E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph)))
27		opeq12 3160	. . . . . 6 |- ((z = A /\ w = B) -> <.z, w>. = <.A, B>.)
28		eceq2 5336	. . . . . 6 |- (<.z, w>. = <.A, B>. -> [<.z, w>.]S = [<.A, B>.]S)
29	27, 28	syl 12	. . . . 5 |- ((z = A /\ w = B) -> [<.z, w>.]S = [<.A, B>.]S)
30		opeq12 3160	. . . . . 6 |- ((v = C /\ u = D) -> <.v, u>. = <.C, D>.)
31		eceq2 5336	. . . . . 6 |- (<.v, u>. = <.C, D>. -> [<.v, u>.]S = [<.C, D>.]S)
32	30, 31	syl 12	. . . . 5 |- ((v = C /\ u = D) -> [<.v, u>.]S = [<.C, D>.]S)
33	29, 32	anim12i 360	. . . 4 |- (((z = A /\ w = B) /\ (v = C /\ u = D)) -> ([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S))
34		opex 3527	. . . . . . . . . 10 |- <.z, w>. e. _V
35		opex 3527	. . . . . . . . . 10 |- <.A, B>. e. _V
36		brecop.2	. . . . . . . . . 10 |- Er S
37		brecop.3	. . . . . . . . . 10 |- dom S = (G X. G)
38	34, 35, 36, 37	ereldm 5343	. . . . . . . . 9 |- ([<.z, w>.]S = [<.A, B>.]S -> (<.z, w>. e. (G X. G) <-> <.A, B>. e. (G X. G)))
39		visset 2295	. . . . . . . . . 10 |- w e. _V
40	39	opelxp 4036	. . . . . . . . 9 |- (<.z, w>. e. (G X. G) <-> (z e. G /\ w e. G))
41	38, 40	syl5bbr 593	. . . . . . . 8 |- ([<.z, w>.]S = [<.A, B>.]S -> ((z e. G /\ w e. G) <-> <.A, B>. e. (G X. G)))
42		opelxpi 4040	. . . . . . . 8 |- ((A e. G /\ B e. G) -> <.A, B>. e. (G X. G))
43	41, 42	syl5bir 227	. . . . . . 7 |- ([<.z, w>.]S = [<.A, B>.]S -> ((A e. G /\ B e. G) -> (z e. G /\ w e. G)))
44		opex 3527	. . . . . . . . . 10 |- <.v, u>. e. _V
45		opex 3527	. . . . . . . . . 10 |- <.C, D>. e. _V
46	44, 45, 36, 37	ereldm 5343	. . . . . . . . 9 |- ([<.v, u>.]S = [<.C, D>.]S -> (<.v, u>. e. (G X. G) <-> <.C, D>. e. (G X. G)))
47		visset 2295	. . . . . . . . . 10 |- u e. _V
48	47	opelxp 4036	. . . . . . . . 9 |- (<.v, u>. e. (G X. G) <-> (v e. G /\ u e. G))
49	46, 48	syl5bbr 593	. . . . . . . 8 |- ([<.v, u>.]S = [<.C, D>.]S -> ((v e. G /\ u e. G) <-> <.C, D>. e. (G X. G)))
50		opelxpi 4040	. . . . . . . 8 |- ((C e. G /\ D e. G) -> <.C, D>. e. (G X. G))
51	49, 50	syl5bir 227	. . . . . . 7 |- ([<.v, u>.]S = [<.C, D>.]S -> ((C e. G /\ D e. G) -> (v e. G /\ u e. G)))
52	43, 51	im2anan9 622	. . . . . 6 |- (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ((z e. G /\ w e. G) /\ (v e. G /\ u e. G))))
53		brecop.6	. . . . . . . . 9 |- ((((z e. G /\ w e. G) /\ (A e. G /\ B e. G)) /\ ((v e. G /\ u e. G) /\ (C e. G /\ D e. G))) -> (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (ph <-> ps)))
54	53	an4s 566	. . . . . . . 8 |- ((((z e. G /\ w e. G) /\ (v e. G /\ u e. G)) /\ ((A e. G /\ B e. G) /\ (C e. G /\ D e. G))) -> (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (ph <-> ps)))
55	54	ex 402	. . . . . . 7 |- (((z e. G /\ w e. G) /\ (v e. G /\ u e. G)) -> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (ph <-> ps))))
56	55	com13 37	. . . . . 6 |- (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (((z e. G /\ w e. G) /\ (v e. G /\ u e. G)) -> (ph <-> ps))))
57	52, 56	mpdd 57	. . . . 5 |- (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (ph <-> ps)))
58	57	pm5.74d 645	. . . 4 |- (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) -> ((((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ph) <-> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ps)))
59	33, 58	cgsex4g 2323	. . 3 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (E.zE.wE.vE.u(([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) /\ (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ph)) <-> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ps)))
60		eqcom 1886	. . . . . . 7 |- ([<.A, B>.]S = [<.z, w>.]S <-> [<.z, w>.]S = [<.A, B>.]S)
61		eqcom 1886	. . . . . . 7 |- ([<.C, D>.]S = [<.v, u>.]S <-> [<.v, u>.]S = [<.C, D>.]S)
62	60, 61	anbi12i 540	. . . . . 6 |- (([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) <-> ([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S))
63	62	a1i 8	. . . . 5 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) <-> ([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S)))
64		biimt 803	. . . . 5 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (ph <-> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ph)))
65	63, 64	anbi12d 690	. . . 4 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ((([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph) <-> (([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) /\ (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ph))))
66	65	4exbidv 1661	. . 3 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph) <-> E.zE.wE.vE.u(([<.z, w>.]S = [<.A, B>.]S /\ [<.v, u>.]S = [<.C, D>.]S) /\ (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ph))))
67		biimt 803	. . 3 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (ps <-> (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ps)))
68	59, 66, 67	3bitr4d 609	. 2 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> (E.zE.wE.vE.u(([<.A, B>.]S = [<.z, w>.]S /\ [<.C, D>.]S = [<.v, u>.]S) /\ ph) <-> ps))
69	26, 68	bitrd 587	1 |- (((A e. G /\ B e. G) /\ (C e. G /\ D e. G)) -> ([<.A, B>.]SR[<.C, D>.]S <-> ps))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292  <.cop 3046   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986  Er wer 5315  [cec 5316  /.cqs 5317

This theorem is referenced by:  ordpipq 6208  ltsrpr 6338

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-er 5318  df-ec 5320  df-qs 5323

Copyright terms: Public domain