Theorem cnvexg

Description: The converse of a set is a set. Corollary 6.8(1) of TakeutiZaring p. 26. (Contributed by NM, 17-Mar-1998)

	Ref	Expression
Assertion	cnvexg	$$⊢A\in V\to A^{-1}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
2		relssdmrn	$$⊢\mathrm{Rel}{A}^{-1}\to A^{-1}\subseteq \mathrm{dom}{A}^{-1}\times \mathrm{ran}{A}^{-1}$$
3	1 2	ax-mp	$$⊢A^{-1}\subseteq \mathrm{dom}{A}^{-1}\times \mathrm{ran}{A}^{-1}$$
4		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
5		rnexg	$$⊢A\in V\to \mathrm{ran}A\in \mathrm{V}$$
6	4 5	eqeltrrid	$$⊢A\in V\to \mathrm{dom}{A}^{-1}\in \mathrm{V}$$
7		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
8		dmexg	$$⊢A\in V\to \mathrm{dom}A\in \mathrm{V}$$
9	7 8	eqeltrrid	$$⊢A\in V\to \mathrm{ran}{A}^{-1}\in \mathrm{V}$$
10	6 9	xpexd	$$⊢A\in V\to \mathrm{dom}{A}^{-1}\times \mathrm{ran}{A}^{-1}\in \mathrm{V}$$
11		ssexg	$$⊢\left(A^{-1}\subseteq \mathrm{dom}{A}^{-1}\times \mathrm{ran}{A}^{-1}\wedge \mathrm{dom}{A}^{-1}\times \mathrm{ran}{A}^{-1}\in \mathrm{V}\right)\to A^{-1}\in \mathrm{V}$$
12	3 10 11	sylancr	$$⊢A\in V\to A^{-1}\in \mathrm{V}$$