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	⊢ ( ( 𝐶 𝐹 𝐴 ) 𝑅 ( 𝐶 𝐹 𝐵 ) → 𝐴 𝑅 𝐵 )