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

Proof

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