Theorem ssltss1

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

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

Proof

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