Theorem maxs2

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	maxs2	|- ( ( A e. No /\ B e. No ) -> B <_s if ( A <_s B , B , A ) )

Proof

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