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 \in No \land B \in No) \to B \leq_{s} if (A \leq_{s} B, B, A)$

Step	Hyp	Ref	Expression
1		slerflex	$⊢ B \in No \to B \leq_{s} B$
2	1	ad2antlr	$⊢ ((A \in No \land B \in No) \land A \leq_{s} B) \to B \leq_{s} B$
3		iftrue	$⊢ A \leq_{s} B \to if (A \leq_{s} B, B, A) = B$
4	3	adantl	$⊢ ((A \in No \land B \in No) \land A \leq_{s} B) \to if (A \leq_{s} B, B, A) = B$
5	2 4	breqtrrd	$⊢ ((A \in No \land B \in No) \land A \leq_{s} B) \to B \leq_{s} if (A \leq_{s} B, B, A)$
6		sletric	$⊢ (A \in No \land B \in No) \to (A \leq_{s} B \lor B \leq_{s} A)$
7	6	orcanai	$⊢ ((A \in No \land B \in No) \land \neg A \leq_{s} B) \to B \leq_{s} A$
8		iffalse	$⊢ \neg A \leq_{s} B \to if (A \leq_{s} B, B, A) = A$
9	8	adantl	$⊢ ((A \in No \land B \in No) \land \neg A \leq_{s} B) \to if (A \leq_{s} B, B, A) = A$
10	7 9	breqtrrd	$⊢ ((A \in No \land B \in No) \land \neg A \leq_{s} B) \to B \leq_{s} if (A \leq_{s} B, B, A)$
11	5 10	pm2.61dan	$⊢ (A \in No \land B \in No) \to B \leq_{s} if (A \leq_{s} B, B, A)$

Metamath Proof Explorer