Theorem sltsex1 28142

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 28141	. 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 3077  Vcvv 3451   ⊆ wss 3899   class class class wbr 5103   No csur 27990   <s clts 27991   <<s cslts 28136

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-slts 28137

This theorem is used by:  ssslts1  28152  ssslts2  28153  conway  28158  cutsval  28159  sltstr  28166  sltsun1  28167  sltsun2  28168  etaslts  28172  etaslts2  28173  cutbdaybnd2lim  28176  lesrec  28178  eqcuts3  28183  madecut  28262  coinitslts  28298  cofcut1  28299  cofcutr  28303  cutlt  28311  addsuniflem  28380  negsunif  28434  sltmuls1  28526  sltmuls2  28527  precsexlem11  28596