Metamath Proof Explorer

Theorem mins1

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

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

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( A <_s B -> if ( A <_s B , A , B ) = A )
2 1 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s B ) -> if ( A <_s B , A , B ) = A )
3 slerflex 
 |-  ( A e. No -> A <_s A )
4 3 ad2antrr 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s B ) -> A <_s A )
5 2 4 eqbrtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ A <_s B ) -> if ( A <_s B , A , B ) <_s A )
6 iffalse 
 |-  ( -. A <_s B -> if ( A <_s B , A , B ) = B )
7 6 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ -. A <_s B ) -> if ( A <_s B , A , B ) = B )
8 sletric 
 |-  ( ( A e. No /\ B e. No ) -> ( A <_s B \/ B <_s A ) )
9 8 orcanai 
 |-  ( ( ( A e. No /\ B e. No ) /\ -. A <_s B ) -> B <_s A )
10 7 9 eqbrtrd 
 |-  ( ( ( A e. No /\ B e. No ) /\ -. A <_s B ) -> if ( A <_s B , A , B ) <_s A )
11 5 10 pm2.61dan 
 |-  ( ( A e. No /\ B e. No ) -> if ( A <_s B , A , B ) <_s A )