Metamath Proof Explorer


Theorem brecop

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

Ref Expression
Hypotheses brecop.1 ˙ V
brecop.2 ˙ Er G × G
brecop.4 H = G × G / ˙
brecop.5 ˙ = x y | x H y H z w v u x = z w ˙ y = v u ˙ φ
brecop.6 z G w G A G B G v G u G C G D G z w ˙ = A B ˙ v u ˙ = C D ˙ φ ψ
Assertion brecop A G B G C G D G A B ˙ ˙ C D ˙ ψ

Proof

Step Hyp Ref Expression
1 brecop.1 ˙ V
2 brecop.2 ˙ Er G × G
3 brecop.4 H = G × G / ˙
4 brecop.5 ˙ = x y | x H y H z w v u x = z w ˙ y = v u ˙ φ
5 brecop.6 z G w G A G B G v G u G C G D G z w ˙ = A B ˙ v u ˙ = C D ˙ φ ψ
6 1 3 ecopqsi A G B G A B ˙ H
7 1 3 ecopqsi C G D G C D ˙ H
8 df-br A B ˙ ˙ C D ˙ A B ˙ C D ˙ ˙
9 4 eleq2i A B ˙ C D ˙ ˙ A B ˙ C D ˙ x y | x H y H z w v u x = z w ˙ y = v u ˙ φ
10 8 9 bitri A B ˙ ˙ C D ˙ A B ˙ C D ˙ x y | x H y H z w v u x = z w ˙ y = v u ˙ φ
11 eqeq1 x = A B ˙ x = z w ˙ A B ˙ = z w ˙
12 11 anbi1d x = A B ˙ x = z w ˙ y = v u ˙ A B ˙ = z w ˙ y = v u ˙
13 12 anbi1d x = A B ˙ x = z w ˙ y = v u ˙ φ A B ˙ = z w ˙ y = v u ˙ φ
14 13 4exbidv x = A B ˙ z w v u x = z w ˙ y = v u ˙ φ z w v u A B ˙ = z w ˙ y = v u ˙ φ
15 eqeq1 y = C D ˙ y = v u ˙ C D ˙ = v u ˙
16 15 anbi2d y = C D ˙ A B ˙ = z w ˙ y = v u ˙ A B ˙ = z w ˙ C D ˙ = v u ˙
17 16 anbi1d y = C D ˙ A B ˙ = z w ˙ y = v u ˙ φ A B ˙ = z w ˙ C D ˙ = v u ˙ φ
18 17 4exbidv y = C D ˙ z w v u A B ˙ = z w ˙ y = v u ˙ φ z w v u A B ˙ = z w ˙ C D ˙ = v u ˙ φ
19 14 18 opelopab2 A B ˙ H C D ˙ H A B ˙ C D ˙ x y | x H y H z w v u x = z w ˙ y = v u ˙ φ z w v u A B ˙ = z w ˙ C D ˙ = v u ˙ φ
20 10 19 syl5bb A B ˙ H C D ˙ H A B ˙ ˙ C D ˙ z w v u A B ˙ = z w ˙ C D ˙ = v u ˙ φ
21 6 7 20 syl2an A G B G C G D G A B ˙ ˙ C D ˙ z w v u A B ˙ = z w ˙ C D ˙ = v u ˙ φ
22 opeq12 z = A w = B z w = A B
23 22 eceq1d z = A w = B z w ˙ = A B ˙
24 opeq12 v = C u = D v u = C D
25 24 eceq1d v = C u = D v u ˙ = C D ˙
26 23 25 anim12i z = A w = B v = C u = D z w ˙ = A B ˙ v u ˙ = C D ˙
27 opelxpi A G B G A B G × G
28 opelxp z w G × G z G w G
29 2 a1i z w ˙ = A B ˙ ˙ Er G × G
30 id z w ˙ = A B ˙ z w ˙ = A B ˙
31 29 30 ereldm z w ˙ = A B ˙ z w G × G A B G × G
32 28 31 bitr3id z w ˙ = A B ˙ z G w G A B G × G
33 27 32 syl5ibr z w ˙ = A B ˙ A G B G z G w G
34 opelxpi C G D G C D G × G
35 opelxp v u G × G v G u G
36 2 a1i v u ˙ = C D ˙ ˙ Er G × G
37 id v u ˙ = C D ˙ v u ˙ = C D ˙
38 36 37 ereldm v u ˙ = C D ˙ v u G × G C D G × G
39 35 38 bitr3id v u ˙ = C D ˙ v G u G C D G × G
40 34 39 syl5ibr v u ˙ = C D ˙ C G D G v G u G
41 33 40 im2anan9 z w ˙ = A B ˙ v u ˙ = C D ˙ A G B G C G D G z G w G v G u G
42 5 an4s z G w G v G u G A G B G C G D G z w ˙ = A B ˙ v u ˙ = C D ˙ φ ψ
43 42 ex z G w G v G u G A G B G C G D G z w ˙ = A B ˙ v u ˙ = C D ˙ φ ψ
44 43 com13 z w ˙ = A B ˙ v u ˙ = C D ˙ A G B G C G D G z G w G v G u G φ ψ
45 41 44 mpdd z w ˙ = A B ˙ v u ˙ = C D ˙ A G B G C G D G φ ψ
46 45 pm5.74d z w ˙ = A B ˙ v u ˙ = C D ˙ A G B G C G D G φ A G B G C G D G ψ
47 26 46 cgsex4g A G B G C G D G z w v u z w ˙ = A B ˙ v u ˙ = C D ˙ A G B G C G D G φ A G B G C G D G ψ
48 eqcom A B ˙ = z w ˙ z w ˙ = A B ˙
49 eqcom C D ˙ = v u ˙ v u ˙ = C D ˙
50 48 49 anbi12i A B ˙ = z w ˙ C D ˙ = v u ˙ z w ˙ = A B ˙ v u ˙ = C D ˙
51 50 a1i A G B G C G D G A B ˙ = z w ˙ C D ˙ = v u ˙ z w ˙ = A B ˙ v u ˙ = C D ˙
52 biimt A G B G C G D G φ A G B G C G D G φ
53 51 52 anbi12d A G B G C G D G A B ˙ = z w ˙ C D ˙ = v u ˙ φ z w ˙ = A B ˙ v u ˙ = C D ˙ A G B G C G D G φ
54 53 4exbidv A G B G C G D G z w v u A B ˙ = z w ˙ C D ˙ = v u ˙ φ z w v u z w ˙ = A B ˙ v u ˙ = C D ˙ A G B G C G D G φ
55 biimt A G B G C G D G ψ A G B G C G D G ψ
56 47 54 55 3bitr4d A G B G C G D G z w v u A B ˙ = z w ˙ C D ˙ = v u ˙ φ ψ
57 21 56 bitrd A G B G C G D G A B ˙ ˙ C D ˙ ψ