Theorem ndmovordi

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

	Ref	Expression
Hypotheses	ndmovordi.2	|- dom F = ( S X. S )
	ndmovordi.4	|- R C_ ( S X. S )
	ndmovordi.5	|- -. (/) e. S
	ndmovordi.6	|- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Assertion	ndmovordi	|- ( ( C F A ) R ( C F B ) -> A R B )

Proof

Step	Hyp	Ref	Expression
1		ndmovordi.2	|- dom F = ( S X. S )
2		ndmovordi.4	|- R C_ ( S X. S )
3		ndmovordi.5	|- -. (/) e. S
4		ndmovordi.6	|- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )
5	2	brel	|- ( ( C F A ) R ( C F B ) -> ( ( C F A ) e. S /\ ( C F B ) e. S ) )
6	5	simpld	|- ( ( C F A ) R ( C F B ) -> ( C F A ) e. S )
7	1 3	ndmovrcl	|- ( ( C F A ) e. S -> ( C e. S /\ A e. S ) )
8	7	simpld	|- ( ( C F A ) e. S -> C e. S )
9	6 8	syl	|- ( ( C F A ) R ( C F B ) -> C e. S )
10	4	biimprd	|- ( C e. S -> ( ( C F A ) R ( C F B ) -> A R B ) )
11	9 10	mpcom	|- ( ( C F A ) R ( C F B ) -> A R B )