Theorem sltsex1

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

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

Proof

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