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 \to A \subseteq No$

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		simpr1	$⊢ ((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 \subseteq No$
3	1 2	sylbi	$⊢ A ≪_{s} B \to A \subseteq No$

Metamath Proof Explorer