Theorem ndmovordi

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

	Ref	Expression
Hypotheses	ndmovordi.2	$$⊢\mathrm{dom}F=S\times S$$
	ndmovordi.4	$$⊢R\subseteq S\times S$$
	ndmovordi.5	$$⊢\neg \varnothing \in S$$
	ndmovordi.6	$$⊢C\in S\to \left(ARB\leftrightarrow \left(CFA\right)R\left(CFB\right)\right)$$
Assertion	ndmovordi	$$⊢\left(CFA\right)R\left(CFB\right)\to ARB$$

Proof

Step	Hyp	Ref	Expression
1		ndmovordi.2	$$⊢\mathrm{dom}F=S\times S$$
2		ndmovordi.4	$$⊢R\subseteq S\times S$$
3		ndmovordi.5	$$⊢\neg \varnothing \in S$$
4		ndmovordi.6	$$⊢C\in S\to \left(ARB\leftrightarrow \left(CFA\right)R\left(CFB\right)\right)$$
5	2	brel	$$⊢\left(CFA\right)R\left(CFB\right)\to \left(CFA\in S\wedge CFB\in S\right)$$
6	5	simpld	$$⊢\left(CFA\right)R\left(CFB\right)\to CFA\in S$$
7	1 3	ndmovrcl	$$⊢CFA\in S\to \left(C\in S\wedge A\in S\right)$$
8	7	simpld	$$⊢CFA\in S\to C\in S$$
9	6 8	syl	$$⊢\left(CFA\right)R\left(CFB\right)\to C\in S$$
10	4	biimprd	$$⊢C\in S\to \left(\left(CFA\right)R\left(CFB\right)\to ARB\right)$$
11	9 10	mpcom	$$⊢\left(CFA\right)R\left(CFB\right)\to ARB$$