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

Metamath Proof Explorer

Theorem ndmovord

Description: Elimination of redundant antecedents in an ordering law. (Contributed by NM, 7-Mar-1996)

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

Proof

Step Hyp Ref Expression
1 ndmov.1 ⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2 ndmovord.4 ⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
3 ndmovord.5 ⊢ ¬ ∅ ∈ 𝑆
4 ndmovord.6 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
5 4 3expia ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) ) )
6 2 brel ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
7 2 brel ⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → ( ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 ∧ ( 𝐶 𝐹 𝐵 ) ∈ 𝑆 ) )
8 1 3 ndmovrcl ⊢ ( ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 → ( 𝐶 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) )
9 8 simprd ⊢ ( ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 → 𝐴 ∈ 𝑆 )
10 1 3 ndmovrcl ⊢ ( ( 𝐶 𝐹 𝐵 ) ∈ 𝑆 → ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
11 10 simprd ⊢ ( ( 𝐶 𝐹 𝐵 ) ∈ 𝑆 → 𝐵 ∈ 𝑆 )
12 9 11 anim12i ⊢ ( ( ( 𝐶 𝐹 𝐴 ) ∈ 𝑆 ∧ ( 𝐶 𝐹 𝐵 ) ∈ 𝑆 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
13 7 12 syl ⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
14 6 13 pm5.21ni ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )
15 14 a1d ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) ) )
16 5 15 pm2.61i ⊢ ( 𝐶 ∈ 𝑆 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) ) )