Theorem cnvfi

Description: If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Assertion	cnvfi	$$⊢A\in \mathrm{Fin}\to A^{-1}\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnvss	$$⊢{A^{-1}}^{-1}\subseteq A$$
2		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge {A^{-1}}^{-1}\subseteq A\right)\to {A^{-1}}^{-1}\in \mathrm{Fin}$$
3	1 2	mpan2	$$⊢A\in \mathrm{Fin}\to {A^{-1}}^{-1}\in \mathrm{Fin}$$
4		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
5		cnvexg	$$⊢A\in \mathrm{Fin}\to A^{-1}\in \mathrm{V}$$
6		cnven	$$⊢\left(\mathrm{Rel}{A}^{-1}\wedge A^{-1}\in \mathrm{V}\right)\to A^{-1}\approx {A^{-1}}^{-1}$$
7	4 5 6	sylancr	$$⊢A\in \mathrm{Fin}\to A^{-1}\approx {A^{-1}}^{-1}$$
8		enfii	$$⊢\left({A^{-1}}^{-1}\in \mathrm{Fin}\wedge A^{-1}\approx {A^{-1}}^{-1}\right)\to A^{-1}\in \mathrm{Fin}$$
9	3 7 8	syl2anc	$$⊢A\in \mathrm{Fin}\to A^{-1}\in \mathrm{Fin}$$