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

Metamath Proof Explorer

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 )