ndmovord

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

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

Step	Hyp	Ref	Expression
1		ndmov.1	$⊢ dom F = S \times S$
2		ndmovord.4	$⊢ R \subseteq S \times S$
3		ndmovord.5	$⊢ \neg \emptyset \in S$
4		ndmovord.6	$⊢ (A \in S \land B \in S \land C \in S) \to (A R B \leftrightarrow (C F A) R (C F B))$
5	4	3expia	$⊢ (A \in S \land B \in S) \to (C \in S \to (A R B \leftrightarrow (C F A) R (C F B)))$
6	2	brel	$⊢ A R B \to (A \in S \land B \in S)$
7	2	brel	$⊢ (C F A) R (C F B) \to (C F A \in S \land C F B \in S)$
8	1 3	ndmovrcl	$⊢ C F A \in S \to (C \in S \land A \in S)$
9	8	simprd	$⊢ C F A \in S \to A \in S$
10	1 3	ndmovrcl	$⊢ C F B \in S \to (C \in S \land B \in S)$
11	10	simprd	$⊢ C F B \in S \to B \in S$
12	9 11	anim12i	$⊢ (C F A \in S \land C F B \in S) \to (A \in S \land B \in S)$
13	7 12	syl	$⊢ (C F A) R (C F B) \to (A \in S \land B \in S)$
14	6 13	pm5.21ni	$⊢ \neg (A \in S \land B \in S) \to (A R B \leftrightarrow (C F A) R (C F B))$
15	14	a1d	$⊢ \neg (A \in S \land B \in S) \to (C \in S \to (A R B \leftrightarrow (C F A) R (C F B)))$
16	5 15	pm2.61i	$⊢ C \in S \to (A R B \leftrightarrow (C F A) R (C F B))$

Metamath Proof Explorer