Metamath Proof Explorer


Theorem brecop2

Description: Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996) (Revised by AV, 12-Jul-2022)

Ref Expression
Hypotheses brecop2.1 dom ˙ = G × G
brecop2.2 H = G × G / ˙
brecop2.3 R H × H
brecop2.4 ˙ G × G
brecop2.5 ¬ G
brecop2.6 dom + ˙ = G × G
brecop2.7 A G B G C G D G A B ˙ R C D ˙ A + ˙ D ˙ B + ˙ C
Assertion brecop2 A B ˙ R C D ˙ A + ˙ D ˙ B + ˙ C

Proof

Step Hyp Ref Expression
1 brecop2.1 dom ˙ = G × G
2 brecop2.2 H = G × G / ˙
3 brecop2.3 R H × H
4 brecop2.4 ˙ G × G
5 brecop2.5 ¬ G
6 brecop2.6 dom + ˙ = G × G
7 brecop2.7 A G B G C G D G A B ˙ R C D ˙ A + ˙ D ˙ B + ˙ C
8 3 brel A B ˙ R C D ˙ A B ˙ H C D ˙ H
9 ecelqsdm dom ˙ = G × G A B ˙ G × G / ˙ A B G × G
10 1 9 mpan A B ˙ G × G / ˙ A B G × G
11 10 2 eleq2s A B ˙ H A B G × G
12 opelxp A B G × G A G B G
13 11 12 sylib A B ˙ H A G B G
14 ecelqsdm dom ˙ = G × G C D ˙ G × G / ˙ C D G × G
15 1 14 mpan C D ˙ G × G / ˙ C D G × G
16 15 2 eleq2s C D ˙ H C D G × G
17 opelxp C D G × G C G D G
18 16 17 sylib C D ˙ H C G D G
19 13 18 anim12i A B ˙ H C D ˙ H A G B G C G D G
20 8 19 syl A B ˙ R C D ˙ A G B G C G D G
21 4 brel A + ˙ D ˙ B + ˙ C A + ˙ D G B + ˙ C G
22 6 5 ndmovrcl A + ˙ D G A G D G
23 6 5 ndmovrcl B + ˙ C G B G C G
24 22 23 anim12i A + ˙ D G B + ˙ C G A G D G B G C G
25 21 24 syl A + ˙ D ˙ B + ˙ C A G D G B G C G
26 an42 A G D G B G C G A G B G C G D G
27 25 26 sylib A + ˙ D ˙ B + ˙ C A G B G C G D G
28 20 27 7 pm5.21nii A B ˙ R C D ˙ A + ˙ D ˙ B + ˙ C