Theorem relcnvexb

Description: A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007)

	Ref	Expression
Assertion	relcnvexb	$$⊢\mathrm{Rel}R\to \left(R\in \mathrm{V}\leftrightarrow R^{-1}\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnvexg	$$⊢R\in \mathrm{V}\to R^{-1}\in \mathrm{V}$$
2		dfrel2	$$⊢\mathrm{Rel}R\leftrightarrow {R^{-1}}^{-1}=R$$
3		cnvexg	$$⊢R^{-1}\in \mathrm{V}\to {R^{-1}}^{-1}\in \mathrm{V}$$
4		eleq1	$$⊢{R^{-1}}^{-1}=R\to \left({R^{-1}}^{-1}\in \mathrm{V}\leftrightarrow R\in \mathrm{V}\right)$$
5	3 4	imbitrid	$$⊢{R^{-1}}^{-1}=R\to \left(R^{-1}\in \mathrm{V}\to R\in \mathrm{V}\right)$$
6	2 5	sylbi	$$⊢\mathrm{Rel}R\to \left(R^{-1}\in \mathrm{V}\to R\in \mathrm{V}\right)$$
7	1 6	impbid2	$$⊢\mathrm{Rel}R\to \left(R\in \mathrm{V}\leftrightarrow R^{-1}\in \mathrm{V}\right)$$