dfrel2

Description: Alternate definition of relation. Exercise 2 of TakeutiZaring p. 25. (Contributed by NM, 29-Dec-1996)

		Ref	Expression
	Assertion	dfrel2	$⊢ Rel R \leftrightarrow {R^{-1}}^{-1} = R$

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel {R^{-1}}^{-1}$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	opelcnv	$⊢ ⟨x, y⟩ \in {R^{-1}}^{-1} \leftrightarrow ⟨y, x⟩ \in R^{-1}$
5	3 2	opelcnv	$⊢ ⟨y, x⟩ \in R^{-1} \leftrightarrow ⟨x, y⟩ \in R$
6	4 5	bitri	$⊢ ⟨x, y⟩ \in {R^{-1}}^{-1} \leftrightarrow ⟨x, y⟩ \in R$
7	6	eqrelriv	$⊢ (Rel {R^{-1}}^{-1} \land Rel R) \to {R^{-1}}^{-1} = R$
8	1 7	mpan	$⊢ Rel R \to {R^{-1}}^{-1} = R$
9		releq	$⊢ {R^{-1}}^{-1} = R \to (Rel {R^{-1}}^{-1} \leftrightarrow Rel R)$
10	1 9	mpbii	$⊢ {R^{-1}}^{-1} = R \to Rel R$
11	8 10	impbii	$⊢ Rel R \leftrightarrow {R^{-1}}^{-1} = R$

Metamath Proof Explorer