Theorem sltsex2

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

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

Proof

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