Metamath Proof Explorer

Theorem sltsex2

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

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