brsslt

Description: Binary relation form of the surreal set less-than relation. (Contributed by Scott Fenton, 8-Dec-2021)

		Ref	Expression
	Assertion	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))$

Step	Hyp	Ref	Expression
1		df-sslt	$⊢ ≪_{s} = \{⟨a, b⟩ \| (a \subseteq No \land b \subseteq No \land \forall x \in a \forall y \in b x <_{s} y)\}$
2	1	bropaex12	$⊢ A ≪_{s} B \to (A \in V \land B \in V)$
3		sseq1	$⊢ a = A \to (a \subseteq No \leftrightarrow A \subseteq No)$
4		raleq	$⊢ a = A \to (\forall x \in a \forall y \in b x <_{s} y \leftrightarrow \forall x \in A \forall y \in b x <_{s} y)$
5	3 4	3anbi13d	$⊢ a = A \to ((a \subseteq No \land b \subseteq No \land \forall x \in a \forall y \in b x <_{s} y) \leftrightarrow (A \subseteq No \land b \subseteq No \land \forall x \in A \forall y \in b x <_{s} y))$
6		sseq1	$⊢ b = B \to (b \subseteq No \leftrightarrow B \subseteq No)$
7		raleq	$⊢ b = B \to (\forall y \in b x <_{s} y \leftrightarrow \forall y \in B x <_{s} y)$
8	7	ralbidv	$⊢ b = B \to (\forall x \in A \forall y \in b x <_{s} y \leftrightarrow \forall x \in A \forall y \in B x <_{s} y)$
9	6 8	3anbi23d	$⊢ b = B \to ((A \subseteq No \land b \subseteq No \land \forall x \in A \forall y \in b x <_{s} y) \leftrightarrow (A \subseteq No \land B \subseteq No \land \forall x \in A \forall y \in B x <_{s} y))$
10	5 9 1	brabg	$⊢ (A \in V \land B \in V) \to (A ≪_{s} B \leftrightarrow (A \subseteq No \land B \subseteq No \land \forall x \in A \forall y \in B x <_{s} y))$
11	2 10	biadanii	$⊢ 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))$

Metamath Proof Explorer