cosscnv

Description: Class of cosets by the converse of R (Contributed by Peter Mazsa, 17-Jun-2020)

		Ref	Expression
	Assertion	cosscnv	$⊢ ≀ R^{-1} = \{⟨x, y⟩ \| \exists u (x R u \land y R u)\}$

Step	Hyp	Ref	Expression
1		df-coss	$⊢ ≀ R^{-1} = \{⟨x, y⟩ \| \exists u (u R^{-1} x \land u R^{-1} y)\}$
2		brcnvg	$⊢ (u \in V \land x \in V) \to (u R^{-1} x \leftrightarrow x R u)$
3	2	el2v	$⊢ u R^{-1} x \leftrightarrow x R u$
4		brcnvg	$⊢ (u \in V \land y \in V) \to (u R^{-1} y \leftrightarrow y R u)$
5	4	el2v	$⊢ u R^{-1} y \leftrightarrow y R u$
6	3 5	anbi12i	$⊢ (u R^{-1} x \land u R^{-1} y) \leftrightarrow (x R u \land y R u)$
7	6	exbii	$⊢ \exists u (u R^{-1} x \land u R^{-1} y) \leftrightarrow \exists u (x R u \land y R u)$
8	7	opabbii	$⊢ \{⟨x, y⟩ \| \exists u (u R^{-1} x \land u R^{-1} y)\} = \{⟨x, y⟩ \| \exists u (x R u \land y R u)\}$
9	1 8	eqtri	$⊢ ≀ R^{-1} = \{⟨x, y⟩ \| \exists u (x R u \land y R u)\}$

Metamath Proof Explorer