Theorem sltsss2 27996

Description: The second argument of surreal set is a set of surreals. (Contributed by Scott Fenton, 8-Dec-2021.)

Assertion

Ref	Expression
sltsss2	⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )

Proof of Theorem sltsss2

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brslts 27992	. 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
2		simpr2 1214	. 2 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) → 𝐵 ⊆ No )
3	1, 2	sylbi 220	1 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2146  ∀wral 3082  Vcvv 3458   ⊆ wss 3908   class class class wbr 5114   No csur 27841   <s clts 27842   <<s cslts 27987

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-slts 27988

This theorem is used by:  ssslts1  28003  ssslts2  28004  conway  28009  sltstr  28017  sltsun1  28018  sltsun2  28019  etaslts  28023  lesrec  28029  ltsrec  28031  eqcuts3  28034  cofslts  28148  coinitslts  28149  cofcut1  28150  cofcutr  28154  cutlt  28162  cutmax  28164  addsuniflem  28231  negsunif  28285  sltmuls1  28377  sltmuls2  28378  mulsuniflem  28379  mulsunif2lem  28399  precsexlem11  28447  renegscl  28728