Metamath Proof Explorer

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 ⊢ A ∈ No ∧ B ∈ No → if A ≤ s B A B ≤ s A

Proof

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