Metamath Proof Explorer

Theorem somincom

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

Ref Expression
Assertion somincom 
|- ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) = if ( B R A , B , A ) )

Proof

Step Hyp Ref Expression
1 so2nr 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> -. ( A R B /\ B R A ) )
2 nan 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> -. ( A R B /\ B R A ) ) <-> ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ A R B ) -> -. B R A ) )
3 1 2 mpbi 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ A R B ) -> -. B R A )
4 3 iffalsed 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ A R B ) -> if ( B R A , B , A ) = A )
5 4 eqcomd 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ A R B ) -> A = if ( B R A , B , A ) )
6 sotric 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( A R B <-> -. ( A = B \/ B R A ) ) )
7 6 con2bid 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( ( A = B \/ B R A ) <-> -. A R B ) )
8 ifeq2 
 |-  ( A = B -> if ( B R A , B , A ) = if ( B R A , B , B ) )
9 ifid 
 |-  if ( B R A , B , B ) = B
10 8 9 eqtr2di 
 |-  ( A = B -> B = if ( B R A , B , A ) )
11 iftrue 
 |-  ( B R A -> if ( B R A , B , A ) = B )
12 11 eqcomd 
 |-  ( B R A -> B = if ( B R A , B , A ) )
13 10 12 jaoi 
 |-  ( ( A = B \/ B R A ) -> B = if ( B R A , B , A ) )
14 7 13 syl6bir 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( -. A R B -> B = if ( B R A , B , A ) ) )
15 14 imp 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ -. A R B ) -> B = if ( B R A , B , A ) )
16 5 15 ifeqda 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) = if ( B R A , B , A ) )