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\in \mathrm{No}\to if\left(A{\le }_{s}B,A,B\right){\le }_{s}B$$

Proof

Step	Hyp	Ref	Expression
1		slerflex	$$⊢B\in \mathrm{No}\to B{\le }_{s}B$$
2		iffalse	$$⊢\neg A{\le }_{s}B\to if\left(A{\le }_{s}B,A,B\right)=B$$
3	2	breq1d	$$⊢\neg A{\le }_{s}B\to \left(if\left(A{\le }_{s}B,A,B\right){\le }_{s}B\leftrightarrow B{\le }_{s}B\right)$$
4	1 3	syl5ibrcom	$$⊢B\in \mathrm{No}\to \left(\neg A{\le }_{s}B\to if\left(A{\le }_{s}B,A,B\right){\le }_{s}B\right)$$
5		iftrue	$$⊢A{\le }_{s}B\to if\left(A{\le }_{s}B,A,B\right)=A$$
6		id	$$⊢A{\le }_{s}B\to A{\le }_{s}B$$
7	5 6	eqbrtrd	$$⊢A{\le }_{s}B\to if\left(A{\le }_{s}B,A,B\right){\le }_{s}B$$
8	4 7	pm2.61d2	$$⊢B\in \mathrm{No}\to if\left(A{\le }_{s}B,A,B\right){\le }_{s}B$$