Theorem dfrel2

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

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

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{R^{-1}}^{-1}$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{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	$$⊢\left(\mathrm{Rel}{R^{-1}}^{-1}\wedge \mathrm{Rel}R\right)\to {R^{-1}}^{-1}=R$$
8	1 7	mpan	$$⊢\mathrm{Rel}R\to {R^{-1}}^{-1}=R$$
9		releq	$$⊢{R^{-1}}^{-1}=R\to \left(\mathrm{Rel}{R^{-1}}^{-1}\leftrightarrow \mathrm{Rel}R\right)$$
10	1 9	mpbii	$$⊢{R^{-1}}^{-1}=R\to \mathrm{Rel}R$$
11	8 10	impbii	$$⊢\mathrm{Rel}R\leftrightarrow {R^{-1}}^{-1}=R$$