Theorem sltsex1 28028

Description: The first argument of surreal set less-than exists. (Contributed by Scott Fenton, 8-Dec-2021.)

Assertion

Ref	Expression
sltsex1	⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)

Proof of Theorem sltsex1

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

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145  ∀wral 3076  Vcvv 3450   ⊆ wss 3899   class class class wbr 5103   No csur 27876   <s clts 27877   <<s cslts 28022

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-slts 28023

This theorem is used by:  ssslts1  28038  ssslts2  28039  conway  28044  cutsval  28045  sltstr  28052  sltsun1  28053  sltsun2  28054  etaslts  28058  etaslts2  28059  cutbdaybnd2lim  28062  lesrec  28064  eqcuts3  28069  madecut  28148  coinitslts  28184  cofcut1  28185  cofcutr  28189  cutlt  28197  addsuniflem  28266  negsunif  28320  sltmuls1  28412  sltmuls2  28413  precsexlem11  28482