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 ∼ = ( 𝐺 × 𝐺 )
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 ⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ∼ 𝑅 [ ⟨ 𝐶 , 𝐷 ⟩ ] ∼ ↔ ( 𝐴 + 𝐷 ) ≤ ( 𝐵 + 𝐶 ) )