Metamath Proof Explorer

Theorem maxs1

Description: A surreal is less than or equal to the maximum of it and another. (Contributed by Scott Fenton, 14-Feb-2025)

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

Proof

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