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 ∼ = ( 𝐺 × 𝐺 )
	brecop2.2	⊢ 𝐻 = ( ( 𝐺 × 𝐺 ) / ∼ )
	brecop2.3	⊢ 𝑅 ⊆ ( 𝐻 × 𝐻 )
	brecop2.4	⊢ ≤ ⊆ ( 𝐺 × 𝐺 )
	brecop2.5	⊢ ¬ ∅ ∈ 𝐺
	brecop2.6	⊢ dom + = ( 𝐺 × 𝐺 )
	brecop2.7	⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ 𝑅 [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) ) )
Assertion	brecop2	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ 𝑅 [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		brecop2.1	⊢ dom ∼ = ( 𝐺 × 𝐺 )
2		brecop2.2	⊢ 𝐻 = ( ( 𝐺 × 𝐺 ) / ∼ )
3		brecop2.3	⊢ 𝑅 ⊆ ( 𝐻 × 𝐻 )
4		brecop2.4	⊢ ≤ ⊆ ( 𝐺 × 𝐺 )
5		brecop2.5	⊢ ¬ ∅ ∈ 𝐺
6		brecop2.6	⊢ dom + = ( 𝐺 × 𝐺 )
7		brecop2.7	⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ 𝑅 [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) ) )
8	3	brel	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ 𝑅 [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ 𝐻 ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ 𝐻 ) )
9		ecelqsdm	⊢ ( ( dom ∼ = ( 𝐺 × 𝐺 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ ( ( 𝐺 × 𝐺 ) / ∼ ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐺 × 𝐺 ) )
10	1 9	mpan	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ ( ( 𝐺 × 𝐺 ) / ∼ ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐺 × 𝐺 ) )
11	10 2	eleq2s	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ 𝐻 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐺 × 𝐺 ) )
12		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) )
13	11 12	sylib	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ 𝐻 → ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) )
14		ecelqsdm	⊢ ( ( dom ∼ = ( 𝐺 × 𝐺 ) ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ ( ( 𝐺 × 𝐺 ) / ∼ ) ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) )
15	1 14	mpan	⊢ ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ ( ( 𝐺 × 𝐺 ) / ∼ ) → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) )
16	15 2	eleq2s	⊢ ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ 𝐻 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) )
17		opelxp	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝐺 × 𝐺 ) ↔ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) )
18	16 17	sylib	⊢ ( [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ 𝐻 → ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) )
19	13 18	anim12i	⊢ ( ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ ∈ 𝐻 ∧ [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ∈ 𝐻 ) → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) )
20	8 19	syl	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ 𝑅 [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) )
21	4	brel	⊢ ( ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) → ( ( 𝐴 + 𝐷 ) ∈ 𝐺 ∧ ( 𝐵 + 𝐶 ) ∈ 𝐺 ) )
22	6 5	ndmovrcl	⊢ ( ( 𝐴 + 𝐷 ) ∈ 𝐺 → ( 𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) )
23	6 5	ndmovrcl	⊢ ( ( 𝐵 + 𝐶 ) ∈ 𝐺 → ( 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺 ) )
24	22 23	anim12i	⊢ ( ( ( 𝐴 + 𝐷 ) ∈ 𝐺 ∧ ( 𝐵 + 𝐶 ) ∈ 𝐺 ) → ( ( 𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ∧ ( 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺 ) ) )
25	21 24	syl	⊢ ( ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) → ( ( 𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ∧ ( 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺 ) ) )
26		an42	⊢ ( ( ( 𝐴 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ∧ ( 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐺 ) ) ↔ ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) )
27	25 26	sylib	⊢ ( ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) → ( ( 𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺 ) ∧ ( 𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺 ) ) )
28	20 27 7	pm5.21nii	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ 𝑅 [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) )