This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 X. G )
brecop2.2 
|- H = ( ( G X. G ) /. .~ )
brecop2.3 
|- R C_ ( H X. H )
brecop2.4 
|- .<_ C_ ( G X. G )
brecop2.5 
|- -. (/) e. G
brecop2.6 
|- dom .+ = ( G X. G )
brecop2.7 
|- ( ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. 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 X. G )
2 brecop2.2 
 |-  H = ( ( G X. G ) /. .~ )
3 brecop2.3 
 |-  R C_ ( H X. H )
4 brecop2.4 
 |-  .<_ C_ ( G X. G )
5 brecop2.5 
 |-  -. (/) e. G
6 brecop2.6 
 |-  dom .+ = ( G X. G )
7 brecop2.7 
 |-  ( ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) -> ( [ <. A , B >. ] .~ R [ <. C , D >. ] .~ <-> ( A .+ D ) .<_ ( B .+ C ) ) )
8 3 brel 
 |-  ( [ <. A , B >. ] .~ R [ <. C , D >. ] .~ -> ( [ <. A , B >. ] .~ e. H /\ [ <. C , D >. ] .~ e. H ) )
9 ecelqsdm 
 |-  ( ( dom .~ = ( G X. G ) /\ [ <. A , B >. ] .~ e. ( ( G X. G ) /. .~ ) ) -> <. A , B >. e. ( G X. G ) )
10 1 9 mpan 
 |-  ( [ <. A , B >. ] .~ e. ( ( G X. G ) /. .~ ) -> <. A , B >. e. ( G X. G ) )
11 10 2 eleq2s 
 |-  ( [ <. A , B >. ] .~ e. H -> <. A , B >. e. ( G X. G ) )
12 opelxp 
 |-  ( <. A , B >. e. ( G X. G ) <-> ( A e. G /\ B e. G ) )
13 11 12 sylib 
 |-  ( [ <. A , B >. ] .~ e. H -> ( A e. G /\ B e. G ) )
14 ecelqsdm 
 |-  ( ( dom .~ = ( G X. G ) /\ [ <. C , D >. ] .~ e. ( ( G X. G ) /. .~ ) ) -> <. C , D >. e. ( G X. G ) )
15 1 14 mpan 
 |-  ( [ <. C , D >. ] .~ e. ( ( G X. G ) /. .~ ) -> <. C , D >. e. ( G X. G ) )
16 15 2 eleq2s 
 |-  ( [ <. C , D >. ] .~ e. H -> <. C , D >. e. ( G X. G ) )
17 opelxp 
 |-  ( <. C , D >. e. ( G X. G ) <-> ( C e. G /\ D e. G ) )
18 16 17 sylib 
 |-  ( [ <. C , D >. ] .~ e. H -> ( C e. G /\ D e. G ) )
19 13 18 anim12i 
 |-  ( ( [ <. A , B >. ] .~ e. H /\ [ <. C , D >. ] .~ e. H ) -> ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) )
20 8 19 syl 
 |-  ( [ <. A , B >. ] .~ R [ <. C , D >. ] .~ -> ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) )
21 4 brel 
 |-  ( ( A .+ D ) .<_ ( B .+ C ) -> ( ( A .+ D ) e. G /\ ( B .+ C ) e. G ) )
22 6 5 ndmovrcl 
 |-  ( ( A .+ D ) e. G -> ( A e. G /\ D e. G ) )
23 6 5 ndmovrcl 
 |-  ( ( B .+ C ) e. G -> ( B e. G /\ C e. G ) )
24 22 23 anim12i 
 |-  ( ( ( A .+ D ) e. G /\ ( B .+ C ) e. G ) -> ( ( A e. G /\ D e. G ) /\ ( B e. G /\ C e. G ) ) )
25 21 24 syl 
 |-  ( ( A .+ D ) .<_ ( B .+ C ) -> ( ( A e. G /\ D e. G ) /\ ( B e. G /\ C e. G ) ) )
26 an42 
 |-  ( ( ( A e. G /\ D e. G ) /\ ( B e. G /\ C e. G ) ) <-> ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) )
27 25 26 sylib 
 |-  ( ( A .+ D ) .<_ ( B .+ C ) -> ( ( A e. G /\ B e. G ) /\ ( C e. G /\ D e. G ) ) )
28 20 27 7 pm5.21nii 
 |-  ( [ <. A , B >. ] .~ R [ <. C , D >. ] .~ <-> ( A .+ D ) .<_ ( B .+ C ) )