Theorem brecop 6132

Description: Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)

Hypotheses

Ref	Expression
brecop.1	|- .~ e. _V
brecop.2	|- .~ Er ( G X. G)
brecop.4	|- H = (( G X. G) /. .~ )
brecop.5	|- .<_ = { <.x , y >. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ 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 >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> (ph <-> ps)))

Assertion

Ref	Expression
brecop	|- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> ([ <.A , B >.] .~ .<_ [ <. C , D >.] .~ <-> 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, .~ ,y,z,w,v,u   x, H,y   z, G,w,v,u   ph,x,y   ps,z,w,v,u

Allowed substitution hints:   ph(z,w,v,u)   ps(x,y)   G(x,y)   H(z,w,v,u)   .<_ (x,y,z,w,v,u)

Proof of Theorem brecop

Step	Hyp	Ref	Expression
1		brecop.1	. . . 4 |- .~ e. _V
2		brecop.4	. . . 4 |- H = (( G X. G) /. .~ )
3	1, 2	ecopqsi 6097	. . 3 |- ((A e. G /\ B e. G) -> [ <.A , B >.] .~ e. H)
4	1, 2	ecopqsi 6097	. . 3 |- (( C e. G /\ D e. G) -> [ <. C , D >.] .~ e. H)
5		df-br 3756	. . . . 5 |- ([ <.A , B >.] .~ .<_ [ <. C , D >.] .~ <-> <.[ <.A , B >.] .~ , [ <. C , D >.] .~ >. e. .<_ )
6		brecop.5	. . . . . 6 |- .<_ = { <.x , y >. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph)) }
7	6	eleq2i 2101	. . . . 5 |- ( <.[ <.A , B >.] .~ , [ <. C , D >.] .~ >. e. .<_ <-> <.[ <.A , B >.] .~ , [ <. C , D >.] .~ >. e. { <.x , y >. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph)) })
8	5, 7	bitri 173	. . . 4 |- ([ <.A , B >.] .~ .<_ [ <. C , D >.] .~ <-> <.[ <.A , B >.] .~ , [ <. C , D >.] .~ >. e. { <.x , y >. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph)) })
9		eqeq1 2043	. . . . . . . 8 |- (x = [ <.A , B >.] .~ -> (x = [ <.z , w >.] .~ <-> [ <.A , B >.] .~ = [ <.z , w >.] .~ ))
10	9	anbi1d 438	. . . . . . 7 |- (x = [ <.A , B >.] .~ -> ((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) <-> ([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ )))
11	10	anbi1d 438	. . . . . 6 |- (x = [ <.A , B >.] .~ -> (((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph) <-> (([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph)))
12	11	4exbidv 1747	. . . . 5 |- (x = [ <.A , B >.] .~ -> (E.zE.wE.vE.u((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph) <-> E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph)))
13		eqeq1 2043	. . . . . . . 8 |- (y = [ <. C , D >.] .~ -> (y = [ <.v , u >.] .~ <-> [ <. C , D >.] .~ = [ <.v , u >.] .~ ))
14	13	anbi2d 437	. . . . . . 7 |- (y = [ <. C , D >.] .~ -> (([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) <-> ([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ )))
15	14	anbi1d 438	. . . . . 6 |- (y = [ <. C , D >.] .~ -> ((([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph) <-> (([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph)))
16	15	4exbidv 1747	. . . . 5 |- (y = [ <. C , D >.] .~ -> (E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph) <-> E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph)))
17	12, 16	opelopab2 3998	. . . 4 |- (([ <.A , B >.] .~ e. H /\ [ <. C , D >.] .~ e. H) -> ( <.[ <.A , B >.] .~ , [ <. C , D >.] .~ >. e. { <.x , y >. | ((x e. H /\ y e. H) /\ E.zE.wE.vE.u((x = [ <.z , w >.] .~ /\ y = [ <.v , u >.] .~ ) /\ ph)) } <-> E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph)))
18	8, 17	syl5bb 181	. . 3 |- (([ <.A , B >.] .~ e. H /\ [ <. C , D >.] .~ e. H) -> ([ <.A , B >.] .~ .<_ [ <. C , D >.] .~ <-> E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph)))
19	3, 4, 18	syl2an 273	. 2 |- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> ([ <.A , B >.] .~ .<_ [ <. C , D >.] .~ <-> E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph)))
20		opeq12 3542	. . . . . 6 |- ((z = A /\ w = B) -> <.z , w >. = <.A , B >.)
21	20	eceq1d 6078	. . . . 5 |- ((z = A /\ w = B) -> [ <.z , w >.] .~ = [ <.A , B >.] .~ )
22		opeq12 3542	. . . . . 6 |- ((v = C /\ u = D) -> <.v , u >. = <. C , D >.)
23	22	eceq1d 6078	. . . . 5 |- ((v = C /\ u = D) -> [ <.v , u >.] .~ = [ <. C , D >.] .~ )
24	21, 23	anim12i 321	. . . 4 |- (((z = A /\ w = B) /\ (v = C /\ u = D)) -> ([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ))
25		opelxpi 4319	. . . . . . . 8 |- ((A e. G /\ B e. G) -> <.A , B >. e. ( G X. G))
26		opelxp 4317	. . . . . . . . 9 |- ( <.z , w >. e. ( G X. G) <-> (z e. G /\ w e. G))
27		brecop.2	. . . . . . . . . . 11 |- .~ Er ( G X. G)
28	27	a1i 9	. . . . . . . . . 10 |- ([ <.z , w >.] .~ = [ <.A , B >.] .~ -> .~ Er ( G X. G))
29		id 19	. . . . . . . . . 10 |- ([ <.z , w >.] .~ = [ <.A , B >.] .~ -> [ <.z , w >.] .~ = [ <.A , B >.] .~ )
30	28, 29	ereldm 6085	. . . . . . . . 9 |- ([ <.z , w >.] .~ = [ <.A , B >.] .~ -> ( <.z , w >. e. ( G X. G) <-> <.A , B >. e. ( G X. G)))
31	26, 30	syl5bbr 183	. . . . . . . 8 |- ([ <.z , w >.] .~ = [ <.A , B >.] .~ -> ((z e. G /\ w e. G) <-> <.A , B >. e. ( G X. G)))
32	25, 31	syl5ibr 145	. . . . . . 7 |- ([ <.z , w >.] .~ = [ <.A , B >.] .~ -> ((A e. G /\ B e. G) -> (z e. G /\ w e. G)))
33		opelxpi 4319	. . . . . . . 8 |- (( C e. G /\ D e. G) -> <. C , D >. e. ( G X. G))
34		opelxp 4317	. . . . . . . . 9 |- ( <.v , u >. e. ( G X. G) <-> (v e. G /\ u e. G))
35	27	a1i 9	. . . . . . . . . 10 |- ([ <.v , u >.] .~ = [ <. C , D >.] .~ -> .~ Er ( G X. G))
36		id 19	. . . . . . . . . 10 |- ([ <.v , u >.] .~ = [ <. C , D >.] .~ -> [ <.v , u >.] .~ = [ <. C , D >.] .~ )
37	35, 36	ereldm 6085	. . . . . . . . 9 |- ([ <.v , u >.] .~ = [ <. C , D >.] .~ -> ( <.v , u >. e. ( G X. G) <-> <. C , D >. e. ( G X. G)))
38	34, 37	syl5bbr 183	. . . . . . . 8 |- ([ <.v , u >.] .~ = [ <. C , D >.] .~ -> ((v e. G /\ u e. G) <-> <. C , D >. e. ( G X. G)))
39	33, 38	syl5ibr 145	. . . . . . 7 |- ([ <.v , u >.] .~ = [ <. C , D >.] .~ -> (( C e. G /\ D e. G) -> (v e. G /\ u e. G)))
40	32, 39	im2anan9 530	. . . . . 6 |- (([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> ((z e. G /\ w e. G) /\ (v e. G /\ u e. G))))
41		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 >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> (ph <-> ps)))
42	41	an4s 522	. . . . . . . 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 >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> (ph <-> ps)))
43	42	ex 108	. . . . . . 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 >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> (ph <-> ps))))
44	43	com13 74	. . . . . 6 |- (([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> (((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))))
45	40, 44	mpdd 36	. . . . 5 |- (([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> (ph <-> ps)))
46	45	pm5.74d 171	. . . 4 |- (([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) -> ((((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)))
47	24, 46	cgsex4g 2585	. . 3 |- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> (E.zE.wE.vE.u(([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) /\ (((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)))
48		eqcom 2039	. . . . . . 7 |- ([ <.A , B >.] .~ = [ <.z , w >.] .~ <-> [ <.z , w >.] .~ = [ <.A , B >.] .~ )
49		eqcom 2039	. . . . . . 7 |- ([ <. C , D >.] .~ = [ <.v , u >.] .~ <-> [ <.v , u >.] .~ = [ <. C , D >.] .~ )
50	48, 49	anbi12i 433	. . . . . 6 |- (([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) <-> ([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ))
51	50	a1i 9	. . . . 5 |- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> (([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) <-> ([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ )))
52		biimt 230	. . . . 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)))
53	51, 52	anbi12d 442	. . . 4 |- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> ((([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph) <-> (([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) /\ (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> ph))))
54	53	4exbidv 1747	. . 3 |- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> (E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph) <-> E.zE.wE.vE.u(([ <.z , w >.] .~ = [ <.A , B >.] .~ /\ [ <.v , u >.] .~ = [ <. C , D >.] .~ ) /\ (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> ph))))
55		biimt 230	. . 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)))
56	47, 54, 55	3bitr4d 209	. 2 |- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> (E.zE.wE.vE.u(([ <.A , B >.] .~ = [ <.z , w >.] .~ /\ [ <. C , D >.] .~ = [ <.v , u >.] .~ ) /\ ph) <-> ps))
57	19, 56	bitrd 177	1 |- (((A e. G /\ B e. G) /\ ( C e. G /\ D e. G)) -> ([ <.A , B >.] .~ .<_ [ <. C , D >.] .~ <-> ps))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551   <.cop 3370   class class class wbr 3755   {copab 3808   X. cxp 4286   Er wer 6039  [cec 6040   /.cqs 6041

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-xp 4294  df-cnv 4296  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-er 6042  df-ec 6044  df-qs 6048

This theorem is referenced by:  ordpipqqs  6358  ltsrprg  6655