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