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

Theorem sletri3 33342
 Description: Trichotomy law for surreal less than or equal. (Contributed by Scott Fenton, 8-Dec-2021.)
Assertion
Ref Expression
sletri3 ((𝐴 No 𝐵 No ) → (𝐴 = 𝐵 ↔ (𝐴 ≤s 𝐵𝐵 ≤s 𝐴)))

Proof of Theorem sletri3
StepHypRef Expression
1 slttrieq2 33337 . 2 ((𝐴 No 𝐵 No ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴)))
2 slenlt 33339 . . . 4 ((𝐴 No 𝐵 No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
3 slenlt 33339 . . . . 5 ((𝐵 No 𝐴 No ) → (𝐵 ≤s 𝐴 ↔ ¬ 𝐴 <s 𝐵))
43ancoms 462 . . . 4 ((𝐴 No 𝐵 No ) → (𝐵 ≤s 𝐴 ↔ ¬ 𝐴 <s 𝐵))
52, 4anbi12d 633 . . 3 ((𝐴 No 𝐵 No ) → ((𝐴 ≤s 𝐵𝐵 ≤s 𝐴) ↔ (¬ 𝐵 <s 𝐴 ∧ ¬ 𝐴 <s 𝐵)))
6 ancom 464 . . 3 ((¬ 𝐵 <s 𝐴 ∧ ¬ 𝐴 <s 𝐵) ↔ (¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴))
75, 6syl6bb 290 . 2 ((𝐴 No 𝐵 No ) → ((𝐴 ≤s 𝐵𝐵 ≤s 𝐴) ↔ (¬ 𝐴 <s 𝐵 ∧ ¬ 𝐵 <s 𝐴)))
81, 7bitr4d 285 1 ((𝐴 No 𝐵 No ) → (𝐴 = 𝐵 ↔ (𝐴 ≤s 𝐵𝐵 ≤s 𝐴)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112   class class class wbr 5033   No csur 33255
 Copyright terms: Public domain W3C validator