Theorem pwfir

Description: If the power set of a set is finite, then the set itself is finite. (Contributed by BTernaryTau, 7-Sep-2024)

	Ref	Expression
Assertion	pwfir	$$⊢𝒫B\in \mathrm{Fin}\to B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$$⊢\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\left[𝒫B\right]=\mathrm{ran}\left({\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\upharpoonright }_{𝒫B}\right)$$
2		relopab	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}$$
3		dmopabss	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\subseteq 𝒫B$$
4		relssres	$$⊢\left(\mathrm{Rel}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\wedge \mathrm{dom}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\subseteq 𝒫B\right)\to {\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\upharpoonright }_{𝒫B}=\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}$$
5	2 3 4	mp2an	$$⊢{\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\upharpoonright }_{𝒫B}=\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}$$
6	5	rneqi	$$⊢\mathrm{ran}\left({\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\upharpoonright }_{𝒫B}\right)=\mathrm{ran}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}$$
7		rnopab	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}=\left\{y|\exists x\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}$$
8		eleq1	$$⊢\left\{y\right\}=x\to \left(\left\{y\right\}\in 𝒫B\leftrightarrow x\in 𝒫B\right)$$
9	8	biimparc	$$⊢\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\to \left\{y\right\}\in 𝒫B$$
10		vex	$$⊢y\in \mathrm{V}$$
11	10	snelpw	$$⊢y\in B\leftrightarrow \left\{y\right\}\in 𝒫B$$
12	9 11	sylibr	$$⊢\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\to y\in B$$
13	12	exlimiv	$$⊢\exists x\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\to y\in B$$
14		snelpwi	$$⊢y\in B\to \left\{y\right\}\in 𝒫B$$
15		eqid	$$⊢\left\{y\right\}=\left\{y\right\}$$
16		eqeq2	$$⊢x=\left\{y\right\}\to \left(\left\{y\right\}=x\leftrightarrow \left\{y\right\}=\left\{y\right\}\right)$$
17	16	rspcev	$$⊢\left(\left\{y\right\}\in 𝒫B\wedge \left\{y\right\}=\left\{y\right\}\right)\to \exists x\in 𝒫B\left\{y\right\}=x$$
18	14 15 17	sylancl	$$⊢y\in B\to \exists x\in 𝒫B\left\{y\right\}=x$$
19		df-rex	$$⊢\exists x\in 𝒫B\left\{y\right\}=x\leftrightarrow \exists x\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)$$
20	18 19	sylib	$$⊢y\in B\to \exists x\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)$$
21	13 20	impbii	$$⊢\exists x\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\leftrightarrow y\in B$$
22	21	abbii	$$⊢\left\{y|\exists x\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}=\left\{y|y\in B\right\}$$
23		abid2	$$⊢\left\{y|y\in B\right\}=B$$
24	7 22 23	3eqtri	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}=B$$
25	1 6 24	3eqtri	$$⊢\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\left[𝒫B\right]=B$$
26		funopab	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\leftrightarrow \forall x{\exists }^{*}y\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)$$
27		mosneq	$$⊢{\exists }^{*}y\left\{y\right\}=x$$
28	27	moani	$$⊢{\exists }^{*}y\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)$$
29	26 28	mpgbir	$$⊢\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}$$
30		imafi	$$⊢\left(\mathrm{Fun}\left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\wedge 𝒫B\in \mathrm{Fin}\right)\to \left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\left[𝒫B\right]\in \mathrm{Fin}$$
31	29 30	mpan	$$⊢𝒫B\in \mathrm{Fin}\to \left\{⟨x,y⟩|\left(x\in 𝒫B\wedge \left\{y\right\}=x\right)\right\}\left[𝒫B\right]\in \mathrm{Fin}$$
32	25 31	eqeltrrid	$$⊢𝒫B\in \mathrm{Fin}\to B\in \mathrm{Fin}$$