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

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

Proof of Theorem sletr
StepHypRef Expression
1 sltletr 32209 . . . . . . 7 ((𝐶 No 𝐴 No 𝐵 No ) → ((𝐶 <s 𝐴𝐴 ≤s 𝐵) → 𝐶 <s 𝐵))
213coml 1122 . . . . . 6 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐶 <s 𝐴𝐴 ≤s 𝐵) → 𝐶 <s 𝐵))
32expcomd 453 . . . . 5 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐴 ≤s 𝐵 → (𝐶 <s 𝐴𝐶 <s 𝐵)))
43imp 444 . . . 4 (((𝐴 No 𝐵 No 𝐶 No ) ∧ 𝐴 ≤s 𝐵) → (𝐶 <s 𝐴𝐶 <s 𝐵))
54con3d 148 . . 3 (((𝐴 No 𝐵 No 𝐶 No ) ∧ 𝐴 ≤s 𝐵) → (¬ 𝐶 <s 𝐵 → ¬ 𝐶 <s 𝐴))
65expimpd 630 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 ≤s 𝐵 ∧ ¬ 𝐶 <s 𝐵) → ¬ 𝐶 <s 𝐴))
7 slenlt 32205 . . . 4 ((𝐵 No 𝐶 No ) → (𝐵 ≤s 𝐶 ↔ ¬ 𝐶 <s 𝐵))
873adant1 1125 . . 3 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐵 ≤s 𝐶 ↔ ¬ 𝐶 <s 𝐵))
98anbi2d 742 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 ≤s 𝐵𝐵 ≤s 𝐶) ↔ (𝐴 ≤s 𝐵 ∧ ¬ 𝐶 <s 𝐵)))
10 slenlt 32205 . . 3 ((𝐴 No 𝐶 No ) → (𝐴 ≤s 𝐶 ↔ ¬ 𝐶 <s 𝐴))
11103adant2 1126 . 2 ((𝐴 No 𝐵 No 𝐶 No ) → (𝐴 ≤s 𝐶 ↔ ¬ 𝐶 <s 𝐴))
126, 9, 113imtr4d 283 1 ((𝐴 No 𝐵 No 𝐶 No ) → ((𝐴 ≤s 𝐵𝐵 ≤s 𝐶) → 𝐴 ≤s 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   ∈ wcel 2140   class class class wbr 4805   No csur 32121
 Copyright terms: Public domain W3C validator