Metamath Proof Explorer


Theorem somin2

Description: Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion somin2
|- ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) ( R u. _I ) B )

Proof

Step Hyp Ref Expression
1 somincom
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) = if ( B R A , B , A ) )
2 somin1
 |-  ( ( R Or X /\ ( B e. X /\ A e. X ) ) -> if ( B R A , B , A ) ( R u. _I ) B )
3 2 ancom2s
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( B R A , B , A ) ( R u. _I ) B )
4 1 3 eqbrtrd
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) ( R u. _I ) B )