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

Theorem sssslt2 33371
 Description: Relationship between surreal set less than and subset. (Contributed by Scott Fenton, 9-Dec-2021.)
Assertion
Ref Expression
sssslt2 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐴 <<s 𝐶)

Proof of Theorem sssslt2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssltex1 33365 . . 3 (𝐴 <<s 𝐵𝐴 ∈ V)
21adantr 484 . 2 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐴 ∈ V)
3 ssltex2 33366 . . . 4 (𝐴 <<s 𝐵𝐵 ∈ V)
43adantr 484 . . 3 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐵 ∈ V)
5 simpr 488 . . 3 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐶𝐵)
64, 5ssexd 5192 . 2 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐶 ∈ V)
7 ssltss1 33367 . . . 4 (𝐴 <<s 𝐵𝐴 No )
87adantr 484 . . 3 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐴 No )
9 ssltss2 33368 . . . . 5 (𝐴 <<s 𝐵𝐵 No )
109adantr 484 . . . 4 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐵 No )
115, 10sstrd 3925 . . 3 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐶 No )
12 ssltsep 33369 . . . . 5 (𝐴 <<s 𝐵 → ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦)
1312adantr 484 . . . 4 ((𝐴 <<s 𝐵𝐶𝐵) → ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦)
14 ssralv 3981 . . . . . 6 (𝐶𝐵 → (∀𝑦𝐵 𝑥 <s 𝑦 → ∀𝑦𝐶 𝑥 <s 𝑦))
155, 14syl 17 . . . . 5 ((𝐴 <<s 𝐵𝐶𝐵) → (∀𝑦𝐵 𝑥 <s 𝑦 → ∀𝑦𝐶 𝑥 <s 𝑦))
1615ralimdv 3145 . . . 4 ((𝐴 <<s 𝐵𝐶𝐵) → (∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦 → ∀𝑥𝐴𝑦𝐶 𝑥 <s 𝑦))
1713, 16mpd 15 . . 3 ((𝐴 <<s 𝐵𝐶𝐵) → ∀𝑥𝐴𝑦𝐶 𝑥 <s 𝑦)
188, 11, 173jca 1125 . 2 ((𝐴 <<s 𝐵𝐶𝐵) → (𝐴 No 𝐶 No ∧ ∀𝑥𝐴𝑦𝐶 𝑥 <s 𝑦))
19 brsslt 33364 . 2 (𝐴 <<s 𝐶 ↔ ((𝐴 ∈ V ∧ 𝐶 ∈ V) ∧ (𝐴 No 𝐶 No ∧ ∀𝑥𝐴𝑦𝐶 𝑥 <s 𝑦)))
202, 6, 18, 19syl21anbrc 1341 1 ((𝐴 <<s 𝐵𝐶𝐵) → 𝐴 <<s 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ⊆ wss 3881   class class class wbr 5030   No csur 33257
 Copyright terms: Public domain W3C validator