Metamath Proof Explorer

Theorem mins2

Description: The minimum of two surreals is less than or equal to the second. (Contributed by Scott Fenton, 14-Feb-2025)

Ref Expression
Assertion mins2 
|- ( B e. No -> if ( A <_s B , A , B ) <_s B )

Proof

Step Hyp Ref Expression
1 slerflex 
 |-  ( B e. No -> B <_s B )
2 iffalse 
 |-  ( -. A <_s B -> if ( A <_s B , A , B ) = B )
3 2 breq1d 
 |-  ( -. A <_s B -> ( if ( A <_s B , A , B ) <_s B <-> B <_s B ) )
4 1 3 syl5ibrcom 
 |-  ( B e. No -> ( -. A <_s B -> if ( A <_s B , A , B ) <_s B ) )
5 iftrue 
 |-  ( A <_s B -> if ( A <_s B , A , B ) = A )
6 id 
 |-  ( A <_s B -> A <_s B )
7 5 6 eqbrtrd 
 |-  ( A <_s B -> if ( A <_s B , A , B ) <_s B )
8 4 7 pm2.61d2 
 |-  ( B e. No -> if ( A <_s B , A , B ) <_s B )