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

Theorem slelttr 33349
 Description: Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021.)
Assertion
Ref Expression
slelttr ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 ≤s 𝐵𝐵 <s 𝐶) → 𝐴 <s 𝐶))

Proof of Theorem slelttr
StepHypRef Expression
1 slenlt 33344 . . . 4 ((𝐴 No 𝐵 No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
213adant3 1129 . . 3 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
32anbi1d 632 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 ≤s 𝐵𝐵 <s 𝐶) ↔ (¬ 𝐵 <s 𝐴𝐵 <s 𝐶)))
4 sltso 33294 . . 3 <s Or No
5 sotr2 5469 . . 3 (( <s Or No ∧ (𝐴 No 𝐵 No 𝐶 No )) → ((¬ 𝐵 <s 𝐴𝐵 <s 𝐶) → 𝐴 <s 𝐶))
64, 5mpan 689 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → ((¬ 𝐵 <s 𝐴𝐵 <s 𝐶) → 𝐴 <s 𝐶))
73, 6sylbid 243 1 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 ≤s 𝐵𝐵 <s 𝐶) → 𝐴 <s 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   ∈ wcel 2111   class class class wbr 5030   Or wor 5437   No csur 33260
 Copyright terms: Public domain W3C validator