ercnv

Description: The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Assertion	ercnv	$⊢ R Er A \to R^{-1} = R$

Step	Hyp	Ref	Expression
1		errel	$⊢ R Er A \to Rel R$
2		relcnv	$⊢ Rel R^{-1}$
3		id	$⊢ R Er A \to R Er A$
4	3	ersymb	$⊢ R Er A \to (y R x \leftrightarrow x R y)$
5		vex	$⊢ x \in V$
6		vex	$⊢ y \in V$
7	5 6	brcnv	$⊢ x R^{-1} y \leftrightarrow y R x$
8		df-br	$⊢ x R^{-1} y \leftrightarrow ⟨x, y⟩ \in R^{-1}$
9	7 8	bitr3i	$⊢ y R x \leftrightarrow ⟨x, y⟩ \in R^{-1}$
10		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
11	4 9 10	3bitr3g	$⊢ R Er A \to (⟨x, y⟩ \in R^{-1} \leftrightarrow ⟨x, y⟩ \in R)$
12	11	eqrelrdv2	$⊢ ((Rel R^{-1} \land Rel R) \land R Er A) \to R^{-1} = R$
13	2 12	mpanl1	$⊢ (Rel R \land R Er A) \to R^{-1} = R$
14	1 13	mpancom	$⊢ R Er A \to R^{-1} = R$

Metamath Proof Explorer