Metamath Proof Explorer

Theorem ssltss2

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

Ref Expression
Assertion ssltss2 ⊢ A ≪ s B → B ⊆ No

Proof

Step Hyp Ref Expression
1 brsslt ⊢ A ≪ s B ↔ A ∈ V ∧ B ∈ V ∧ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y
2 simpr2 ⊢ A ∈ V ∧ B ∈ V ∧ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y → B ⊆ No
3 1 2 sylbi ⊢ A ≪ s B → B ⊆ No