Metamath Proof Explorer

Theorem somin1

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

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

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( A R B -> if ( A R B , A , B ) = A )
2 1 olcd 
 |-  ( A R B -> ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) )
3 2 adantl 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ A R B ) -> ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) )
4 sotric 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( A R B <-> -. ( A = B \/ B R A ) ) )
5 orcom 
 |-  ( ( A = B \/ B R A ) <-> ( B R A \/ A = B ) )
6 eqcom 
 |-  ( A = B <-> B = A )
7 6 orbi2i 
 |-  ( ( B R A \/ A = B ) <-> ( B R A \/ B = A ) )
8 5 7 bitri 
 |-  ( ( A = B \/ B R A ) <-> ( B R A \/ B = A ) )
9 8 notbii 
 |-  ( -. ( A = B \/ B R A ) <-> -. ( B R A \/ B = A ) )
10 4 9 bitrdi 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( A R B <-> -. ( B R A \/ B = A ) ) )
11 10 con2bid 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( ( B R A \/ B = A ) <-> -. A R B ) )
12 11 biimpar 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ -. A R B ) -> ( B R A \/ B = A ) )
13 iffalse 
 |-  ( -. A R B -> if ( A R B , A , B ) = B )
14 breq1 
 |-  ( if ( A R B , A , B ) = B -> ( if ( A R B , A , B ) R A <-> B R A ) )
15 eqeq1 
 |-  ( if ( A R B , A , B ) = B -> ( if ( A R B , A , B ) = A <-> B = A ) )
16 14 15 orbi12d 
 |-  ( if ( A R B , A , B ) = B -> ( ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) <-> ( B R A \/ B = A ) ) )
17 13 16 syl 
 |-  ( -. A R B -> ( ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) <-> ( B R A \/ B = A ) ) )
18 17 adantl 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ -. A R B ) -> ( ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) <-> ( B R A \/ B = A ) ) )
19 12 18 mpbird 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X ) ) /\ -. A R B ) -> ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) )
20 3 19 pm2.61dan 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) )
21 poleloe 
 |-  ( A e. X -> ( if ( A R B , A , B ) ( R u. _I ) A <-> ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) ) )
22 21 ad2antrl 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> ( if ( A R B , A , B ) ( R u. _I ) A <-> ( if ( A R B , A , B ) R A \/ if ( A R B , A , B ) = A ) ) )
23 20 22 mpbird 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X ) ) -> if ( A R B , A , B ) ( R u. _I ) A )