Metamath Proof Explorer

Theorem ssltex1

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

Ref Expression
Assertion ssltex1 ⊢ A ≪ s B → A ∈ V

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