Metamath Proof Explorer

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 ⊢ A ≪ s B → A ⊆ 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 simpr1 ⊢ A ∈ V ∧ B ∈ V ∧ A ⊆ No ∧ B ⊆ No ∧ ∀ x ∈ A ∀ y ∈ B x < s y → A ⊆ No
3 1 2 sylbi ⊢ A ≪ s B → A ⊆ No