Theorem sltssep

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

	Ref	Expression
Assertion	sltssep	⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )

Proof

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