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

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

Proof of Theorem sltletr
StepHypRef Expression
1 slenlt 33345 . . . 4 ((𝐵 No 𝐶 No ) → (𝐵 ≤s 𝐶 ↔ ¬ 𝐶 <s 𝐵))
213adant1 1127 . . 3 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐵 ≤s 𝐶 ↔ ¬ 𝐶 <s 𝐵))
32anbi2d 631 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 <s 𝐵𝐵 ≤s 𝐶) ↔ (𝐴 <s 𝐵 ∧ ¬ 𝐶 <s 𝐵)))
4 sltso 33295 . . 3 <s Or No
5 sotr3 33116 . . 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 2112   class class class wbr 5033   Or wor 5441   No csur 33261
 Copyright terms: Public domain W3C validator