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 \to A \in V$

Step	Hyp	Ref	Expression
1		brsslt	$⊢ A ≪_{s} B \leftrightarrow ((A \in V \land B \in V) \land (A \subseteq No \land B \subseteq No \land \forall x \in A \forall y \in B x <_{s} y))$
2		simpll	$⊢ ((A \in V \land B \in V) \land (A \subseteq No \land B \subseteq No \land \forall x \in A \forall y \in B x <_{s} y)) \to A \in V$
3	1 2	sylbi	$⊢ A ≪_{s} B \to A \in V$

Metamath Proof Explorer