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

Metamath Proof Explorer

Theorem ndmovordi

Description: Elimination of redundant antecedent in an ordering law. (Contributed by NM, 25-Jun-1998)

Ref Expression
Hypotheses ndmovordi.2 ⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
ndmovordi.4 ⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
ndmovordi.5 ⊢ ¬ ∅ ∈ 𝑆
ndmovordi.6 ⊢ ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
Assertion ndmovordi ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → 𝐴 𝑅 𝐵 )

Proof

Step Hyp Ref Expression
1 ndmovordi.2 ⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2 ndmovordi.4 ⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
3 ndmovordi.5 ⊢ ¬ ∅ ∈ 𝑆
4 ndmovordi.6 ⊢ ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
5 2 brel ⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → ( ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 ∧ ( 𝐶 𝐹 𝐵 ) ∈ 𝑆 ) )
6 5 simpld ⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 )
7 1 3 ndmovrcl ⊢ ( ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 → ( 𝐶 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) )
8 7 simpld ⊢ ( ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 → 𝐶 ∈ 𝑆 )
9 6 8 syl ⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → 𝐶 ∈ 𝑆 )
10 4 biimprd ⊢ ( 𝐶 ∈ 𝑆 → ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → 𝐴 𝑅 𝐵 ) )
11 9 10 mpcom ⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → 𝐴 𝑅 𝐵 )