Theorem ndmovord

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

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

Proof

Step	Hyp	Ref	Expression
1		ndmov.1	|- dom F = ( S X. S )
2		ndmovord.4	|- R C_ ( S X. S )
3		ndmovord.5	|- -. (/) e. S
4		ndmovord.6	|- ( ( A e. S /\ B e. S /\ C e. S ) -> ( A R B <-> ( C F A ) R ( C F B ) ) )
5	4	3expia	|- ( ( A e. S /\ B e. S ) -> ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) ) )
6	2	brel	|- ( A R B -> ( A e. S /\ B e. S ) )
7	2	brel	|- ( ( C F A ) R ( C F B ) -> ( ( C F A ) e. S /\ ( C F B ) e. S ) )
8	1 3	ndmovrcl	|- ( ( C F A ) e. S -> ( C e. S /\ A e. S ) )
9	8	simprd	|- ( ( C F A ) e. S -> A e. S )
10	1 3	ndmovrcl	|- ( ( C F B ) e. S -> ( C e. S /\ B e. S ) )
11	10	simprd	|- ( ( C F B ) e. S -> B e. S )
12	9 11	anim12i	|- ( ( ( C F A ) e. S /\ ( C F B ) e. S ) -> ( A e. S /\ B e. S ) )
13	7 12	syl	|- ( ( C F A ) R ( C F B ) -> ( A e. S /\ B e. S ) )
14	6 13	pm5.21ni	|- ( -. ( A e. S /\ B e. S ) -> ( A R B <-> ( C F A ) R ( C F B ) ) )
15	14	a1d	|- ( -. ( A e. S /\ B e. S ) -> ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) ) )
16	5 15	pm2.61i	|- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )