Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sltgtso Structured version   Visualization version   GIF version

Theorem sltgtso 31622
 Description: Either the greater than or less than relationship strictly order the surreals. (Contributed by Scott Fenton, 24-Nov-2021.)
Hypothesis
Ref Expression
nominmaxso.1 ( < = <s ∨ < = <s )
Assertion
Ref Expression
sltgtso < Or No

Proof of Theorem sltgtso
StepHypRef Expression
1 nominmaxso.1 . 2 ( < = <s ∨ < = <s )
2 sltso 31582 . . . 4 <s Or No
3 soeq1 5024 . . . 4 ( < = <s → ( < Or No ↔ <s Or No ))
42, 3mpbiri 248 . . 3 ( < = <s → < Or No )
5 socnv 31416 . . . . 5 ( <s Or No <s Or No )
62, 5ax-mp 5 . . . 4 <s Or No
7 soeq1 5024 . . . 4 ( < = <s → ( < Or No <s Or No ))
86, 7mpbiri 248 . . 3 ( < = <s → < Or No )
94, 8jaoi 394 . 2 (( < = <s ∨ < = <s ) → < Or No )
101, 9ax-mp 5 1 < Or No
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 383   = wceq 1480   Or wor 5004  ◡ccnv 5083   No csur 31547
 Copyright terms: Public domain W3C validator