Theorem cnvfi

Description: If a set is finite, its converse is as well. (Contributed by Mario Carneiro, 28-Dec-2014) Avoid ax-pow . (Revised by BTernaryTau, 9-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cnveq	$$⊢x=\varnothing \to x^{-1}={\varnothing }^{-1}$$
2	1	eleq1d	$$⊢x=\varnothing \to \left(x^{-1}\in \mathrm{Fin}\leftrightarrow {\varnothing }^{-1}\in \mathrm{Fin}\right)$$
3		cnveq	$$⊢x=y\to x^{-1}=y^{-1}$$
4	3	eleq1d	$$⊢x=y\to \left(x^{-1}\in \mathrm{Fin}\leftrightarrow y^{-1}\in \mathrm{Fin}\right)$$
5		cnveq	$$⊢x=y\cup \left\{z\right\}\to x^{-1}={\left(y\cup \left\{z\right\}\right)}^{-1}$$
6	5	eleq1d	$$⊢x=y\cup \left\{z\right\}\to \left(x^{-1}\in \mathrm{Fin}\leftrightarrow {\left(y\cup \left\{z\right\}\right)}^{-1}\in \mathrm{Fin}\right)$$
7		cnveq	$$⊢x=A\to x^{-1}=A^{-1}$$
8	7	eleq1d	$$⊢x=A\to \left(x^{-1}\in \mathrm{Fin}\leftrightarrow A^{-1}\in \mathrm{Fin}\right)$$
9		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
10		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
11	9 10	eqeltri	$$⊢{\varnothing }^{-1}\in \mathrm{Fin}$$
12		cnvun	$$⊢{\left(y\cup \left\{z\right\}\right)}^{-1}=y^{-1}\cup {\left\{z\right\}}^{-1}$$
13		elvv	$$⊢z\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists u\exists vz=⟨u,v⟩$$
14		sneq	$$⊢z=⟨u,v⟩\to \left\{z\right\}=\left\{⟨u,v⟩\right\}$$
15		cnveq	$$⊢\left\{z\right\}=\left\{⟨u,v⟩\right\}\to {\left\{z\right\}}^{-1}={\left\{⟨u,v⟩\right\}}^{-1}$$
16		vex	$$⊢u\in \mathrm{V}$$
17		vex	$$⊢v\in \mathrm{V}$$
18	16 17	cnvsn	$$⊢{\left\{⟨u,v⟩\right\}}^{-1}=\left\{⟨v,u⟩\right\}$$
19	15 18	eqtrdi	$$⊢\left\{z\right\}=\left\{⟨u,v⟩\right\}\to {\left\{z\right\}}^{-1}=\left\{⟨v,u⟩\right\}$$
20	14 19	syl	$$⊢z=⟨u,v⟩\to {\left\{z\right\}}^{-1}=\left\{⟨v,u⟩\right\}$$
21		snfi	$$⊢\left\{⟨v,u⟩\right\}\in \mathrm{Fin}$$
22	20 21	eqeltrdi	$$⊢z=⟨u,v⟩\to {\left\{z\right\}}^{-1}\in \mathrm{Fin}$$
23	22	exlimivv	$$⊢\exists u\exists vz=⟨u,v⟩\to {\left\{z\right\}}^{-1}\in \mathrm{Fin}$$
24	13 23	sylbi	$$⊢z\in \left(\mathrm{V}\times \mathrm{V}\right)\to {\left\{z\right\}}^{-1}\in \mathrm{Fin}$$
25		dfdm4	$$⊢\mathrm{dom}\left\{z\right\}=\mathrm{ran}{\left\{z\right\}}^{-1}$$
26		dmsnn0	$$⊢z\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{dom}\left\{z\right\}\ne \varnothing$$
27	26	biimpri	$$⊢\mathrm{dom}\left\{z\right\}\ne \varnothing \to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
28	27	necon1bi	$$⊢\neg z\in \left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{dom}\left\{z\right\}=\varnothing$$
29	25 28	eqtr3id	$$⊢\neg z\in \left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{ran}{\left\{z\right\}}^{-1}=\varnothing$$
30		relcnv	$$⊢\mathrm{Rel}{\left\{z\right\}}^{-1}$$
31		relrn0	$$⊢\mathrm{Rel}{\left\{z\right\}}^{-1}\to \left({\left\{z\right\}}^{-1}=\varnothing \leftrightarrow \mathrm{ran}{\left\{z\right\}}^{-1}=\varnothing \right)$$
32	30 31	ax-mp	$$⊢{\left\{z\right\}}^{-1}=\varnothing \leftrightarrow \mathrm{ran}{\left\{z\right\}}^{-1}=\varnothing$$
33	29 32	sylibr	$$⊢\neg z\in \left(\mathrm{V}\times \mathrm{V}\right)\to {\left\{z\right\}}^{-1}=\varnothing$$
34	33 10	eqeltrdi	$$⊢\neg z\in \left(\mathrm{V}\times \mathrm{V}\right)\to {\left\{z\right\}}^{-1}\in \mathrm{Fin}$$
35	24 34	pm2.61i	$$⊢{\left\{z\right\}}^{-1}\in \mathrm{Fin}$$
36		unfi	$$⊢\left(y^{-1}\in \mathrm{Fin}\wedge {\left\{z\right\}}^{-1}\in \mathrm{Fin}\right)\to y^{-1}\cup {\left\{z\right\}}^{-1}\in \mathrm{Fin}$$
37	35 36	mpan2	$$⊢y^{-1}\in \mathrm{Fin}\to y^{-1}\cup {\left\{z\right\}}^{-1}\in \mathrm{Fin}$$
38	12 37	eqeltrid	$$⊢y^{-1}\in \mathrm{Fin}\to {\left(y\cup \left\{z\right\}\right)}^{-1}\in \mathrm{Fin}$$
39	38	a1i	$$⊢y\in \mathrm{Fin}\to \left(y^{-1}\in \mathrm{Fin}\to {\left(y\cup \left\{z\right\}\right)}^{-1}\in \mathrm{Fin}\right)$$
40	2 4 6 8 11 39	findcard2	$$⊢A\in \mathrm{Fin}\to A^{-1}\in \mathrm{Fin}$$