Theorem sltsex1 27759

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 27758	. 2 ⊢ (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
2		simpll 766	. 2 ⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)) → 𝐴 ∈ V)
3	1, 2	sylbi 217	1 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   ⊆ wss 3901   class class class wbr 5098   No csur 27607   <s clts 27608   <<s cslts 27753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-slts 27754

This theorem is referenced by:  ssslts1  27769  ssslts2  27770  conway  27775  cutsval  27776  sltstr  27783  sltsun1  27784  sltsun2  27785  etaslts  27789  etaslts2  27790  cutbdaybnd2lim  27793  lesrec  27795  eqcuts3  27800  madecut  27879  coinitslts  27915  cofcut1  27916  cofcutr  27920  cutlt  27928  addsuniflem  27997  negsunif  28051  sltmuls1  28143  sltmuls2  28144  precsexlem11  28213