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 ) )