ndmovordi

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

	Ref	Expression
Hypotheses	ndmovordi.2	$⊢ dom F = S \times S$
	ndmovordi.4	$⊢ R \subseteq S \times S$
	ndmovordi.5	$⊢ \neg \emptyset \in S$
	ndmovordi.6	$⊢ C \in S \to (A R B \leftrightarrow (C F A) R (C F B))$
Assertion	ndmovordi	$⊢ (C F A) R (C F B) \to A R B$

Step	Hyp	Ref	Expression
1		ndmovordi.2	$⊢ dom F = S \times S$
2		ndmovordi.4	$⊢ R \subseteq S \times S$
3		ndmovordi.5	$⊢ \neg \emptyset \in S$
4		ndmovordi.6	$⊢ C \in S \to (A R B \leftrightarrow (C F A) R (C F B))$
5	2	brel	$⊢ (C F A) R (C F B) \to (C F A \in S \land C F B \in S)$
6	5	simpld	$⊢ (C F A) R (C F B) \to C F A \in S$
7	1 3	ndmovrcl	$⊢ C F A \in S \to (C \in S \land A \in S)$
8	7	simpld	$⊢ C F A \in S \to C \in S$
9	6 8	syl	$⊢ (C F A) R (C F B) \to C \in S$
10	4	biimprd	$⊢ C \in S \to ((C F A) R (C F B) \to A R B)$
11	9 10	mpcom	$⊢ (C F A) R (C F B) \to A R B$

Metamath Proof Explorer