Theorem sltsss2

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

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

Proof

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