Theorem cnvct

Description: If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016)

	Ref	Expression
Assertion	cnvct	$$⊢A\preccurlyeq \mathrm{\omega }\to A^{-1}\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
2		ctex	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$
3		cnvexg	$$⊢A\in \mathrm{V}\to A^{-1}\in \mathrm{V}$$
4	2 3	syl	$$⊢A\preccurlyeq \mathrm{\omega }\to A^{-1}\in \mathrm{V}$$
5		cnven	$$⊢\left(\mathrm{Rel}{A}^{-1}\wedge A^{-1}\in \mathrm{V}\right)\to A^{-1}\approx {A^{-1}}^{-1}$$
6	1 4 5	sylancr	$$⊢A\preccurlyeq \mathrm{\omega }\to A^{-1}\approx {A^{-1}}^{-1}$$
7		cnvcnvss	$$⊢{A^{-1}}^{-1}\subseteq A$$
8		ssdomg	$$⊢A\in \mathrm{V}\to \left({A^{-1}}^{-1}\subseteq A\to {A^{-1}}^{-1}\preccurlyeq A\right)$$
9	2 7 8	mpisyl	$$⊢A\preccurlyeq \mathrm{\omega }\to {A^{-1}}^{-1}\preccurlyeq A$$
10		endomtr	$$⊢\left(A^{-1}\approx {A^{-1}}^{-1}\wedge {A^{-1}}^{-1}\preccurlyeq A\right)\to A^{-1}\preccurlyeq A$$
11	6 9 10	syl2anc	$$⊢A\preccurlyeq \mathrm{\omega }\to A^{-1}\preccurlyeq A$$
12		domtr	$$⊢\left(A^{-1}\preccurlyeq A\wedge A\preccurlyeq \mathrm{\omega }\right)\to A^{-1}\preccurlyeq \mathrm{\omega }$$
13	11 12	mpancom	$$⊢A\preccurlyeq \mathrm{\omega }\to A^{-1}\preccurlyeq \mathrm{\omega }$$