prjsprel

Description: Utility theorem regarding the relation used in PrjSp . (Contributed by Steven Nguyen, 29-Apr-2023)

		Ref	Expression
	Hypothesis	prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
	Assertion	prjsprel	$⊢ X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y)$

Step	Hyp	Ref	Expression
1		prjsprel.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land \exists l \in K x = l \underset{˙}{\cdot} y)\}$
2		simpll	$⊢ ((x = X \land y = Y) \land l = m) \to x = X$
3		simpr	$⊢ ((x = X \land y = Y) \land l = m) \to l = m$
4		simplr	$⊢ ((x = X \land y = Y) \land l = m) \to y = Y$
5	3 4	oveq12d	$⊢ ((x = X \land y = Y) \land l = m) \to l \underset{˙}{\cdot} y = m \underset{˙}{\cdot} Y$
6	2 5	eqeq12d	$⊢ ((x = X \land y = Y) \land l = m) \to (x = l \underset{˙}{\cdot} y \leftrightarrow X = m \underset{˙}{\cdot} Y)$
7	6	cbvrexdva	$⊢ (x = X \land y = Y) \to (\exists l \in K x = l \underset{˙}{\cdot} y \leftrightarrow \exists m \in K X = m \underset{˙}{\cdot} Y)$
8	7 1	brab2a	$⊢ X \underset{˙}{\sim} Y \leftrightarrow ((X \in B \land Y \in B) \land \exists m \in K X = m \underset{˙}{\cdot} Y)$

Metamath Proof Explorer