This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )