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	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ≤s if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		lesid	⊢ ( 𝐵 ∈ No → 𝐵 ≤s 𝐵 )
2	1	ad2antlr	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 ≤s 𝐵 ) → 𝐵 ≤s 𝐵 )
3		iftrue	⊢ ( 𝐴 ≤s 𝐵 → if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
4	3	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 ≤s 𝐵 ) → if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) = 𝐵 )
5	2 4	breqtrrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 ≤s 𝐵 ) → 𝐵 ≤s if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) )
6		lestric	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ∨ 𝐵 ≤s 𝐴 ) )
7	6	orcanai	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴 ≤s 𝐵 ) → 𝐵 ≤s 𝐴 )
8		iffalse	⊢ ( ¬ 𝐴 ≤s 𝐵 → if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) = 𝐴 )
9	8	adantl	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴 ≤s 𝐵 ) → if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) = 𝐴 )
10	7 9	breqtrrd	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴 ≤s 𝐵 ) → 𝐵 ≤s if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) )
11	5 10	pm2.61dan	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ≤s if ( 𝐴 ≤s 𝐵 , 𝐵 , 𝐴 ) )