Metamath Proof Explorer

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

Proof

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