Metamath Proof Explorer

Theorem sltsex1

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

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

Proof

Step Hyp Ref Expression
1 brslts ⊢ 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