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→ifA≤sBAB≤sA

Proof

Step Hyp Ref Expression
1 iftrue ⊢A≤sB→ifA≤sBAB=A
2 1 adantl ⊢A∈No∧B∈No∧A≤sB→ifA≤sBAB=A
3 slerflex ⊢A∈No→A≤sA
4 3 ad2antrr ⊢A∈No∧B∈No∧A≤sB→A≤sA
5 2 4 eqbrtrd ⊢A∈No∧B∈No∧A≤sB→ifA≤sBAB≤sA
6 iffalse ⊢¬A≤sB→ifA≤sBAB=B
7 6 adantl ⊢A∈No∧B∈No∧¬A≤sB→ifA≤sBAB=B
8 sletric ⊢A∈No∧B∈No→A≤sB∨B≤sA
9 8 orcanai ⊢A∈No∧B∈No∧¬A≤sB→B≤sA
10 7 9 eqbrtrd ⊢A∈No∧B∈No∧¬A≤sB→ifA≤sBAB≤sA
11 5 10 pm2.61dan ⊢A∈No∧B∈No→ifA≤sBAB≤sA