Theorem cnven

Description: A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Assertion	cnven	$$⊢\left(\mathrm{Rel}A\wedge A\in V\right)\to A\approx A^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(\mathrm{Rel}A\wedge A\in V\right)\to A\in V$$
2		cnvexg	$$⊢A\in V\to A^{-1}\in \mathrm{V}$$
3	2	adantl	$$⊢\left(\mathrm{Rel}A\wedge A\in V\right)\to A^{-1}\in \mathrm{V}$$
4		cnvf1o	$$⊢\mathrm{Rel}A\to \left(x\in A⟼\bigcup {\left\{x\right\}}^{-1}\right):A\underset{1-1\; onto}{⟶}{A}^{-1}$$
5	4	adantr	$$⊢\left(\mathrm{Rel}A\wedge A\in V\right)\to \left(x\in A⟼\bigcup {\left\{x\right\}}^{-1}\right):A\underset{1-1\; onto}{⟶}{A}^{-1}$$
6		f1oen2g	$$⊢\left(A\in V\wedge A^{-1}\in \mathrm{V}\wedge \left(x\in A⟼\bigcup {\left\{x\right\}}^{-1}\right):A\underset{1-1\; onto}{⟶}{A}^{-1}\right)\to A\approx A^{-1}$$
7	1 3 5 6	syl3anc	$$⊢\left(\mathrm{Rel}A\wedge A\in V\right)\to A\approx A^{-1}$$