rp-brsslt

Description: Binary relation form of a relation, .< , which has been extended from relation R to subsets of class S . Usually, we will assume R Or S . Definition in Alling, p. 2. Generalization of brsslt . (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023)

		Ref	Expression
	Hypothesis	nla0001.defsslt	$⊢ \underset{˙}{<} = \{⟨a, b⟩ \| (a \subseteq S \land b \subseteq S \land \forall x \in a \forall y \in b x R y)\}$
	Assertion	rp-brsslt	$⊢ A \underset{˙}{<} B \leftrightarrow ((A \in V \land B \in V) \land (A \subseteq S \land B \subseteq S \land \forall x \in A \forall y \in B x R y))$

Proof

Step	Hyp	Ref	Expression
1		nla0001.defsslt	$⊢ \underset{˙}{<} = \{⟨a, b⟩ \| (a \subseteq S \land b \subseteq S \land \forall x \in a \forall y \in b x R y)\}$
2		sseq1	$⊢ a = A \to (a \subseteq S \leftrightarrow A \subseteq S)$
3		raleq	$⊢ a = A \to (\forall x \in a \forall y \in b x R y \leftrightarrow \forall x \in A \forall y \in b x R y)$
4	2 3	3anbi13d	$⊢ a = A \to ((a \subseteq S \land b \subseteq S \land \forall x \in a \forall y \in b x R y) \leftrightarrow (A \subseteq S \land b \subseteq S \land \forall x \in A \forall y \in b x R y))$
5		sseq1	$⊢ b = B \to (b \subseteq S \leftrightarrow B \subseteq S)$
6		raleq	$⊢ b = B \to (\forall y \in b x R y \leftrightarrow \forall y \in B x R y)$
7	6	ralbidv	$⊢ b = B \to (\forall x \in A \forall y \in b x R y \leftrightarrow \forall x \in A \forall y \in B x R y)$
8	5 7	3anbi23d	$⊢ b = B \to ((A \subseteq S \land b \subseteq S \land \forall x \in A \forall y \in b x R y) \leftrightarrow (A \subseteq S \land B \subseteq S \land \forall x \in A \forall y \in B x R y))$
9	4 8 1	bropabg	$⊢ A \underset{˙}{<} B \leftrightarrow ((A \in V \land B \in V) \land (A \subseteq S \land B \subseteq S \land \forall x \in A \forall y \in B x R y))$

Metamath Proof Explorer

Theorem rp-brsslt

Proof