Theorem isfin3

Description: Definition of a III-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin3	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow 𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}$$

Proof

Step	Hyp	Ref	Expression
1		df-fin3	$$⊢{\mathrm{Fin}}^{\mathrm{III}}=\left\{x|𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}\right\}$$
2	1	eleq2i	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow A\in \left\{x|𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}\right\}$$
3		pwexr	$$⊢𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}\to A\in \mathrm{V}$$
4		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
5	4	eleq1d	$$⊢x=A\to \left(𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow 𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}\right)$$
6	3 5	elab3	$$⊢A\in \left\{x|𝒫x\in {\mathrm{Fin}}^{\mathrm{IV}}\right\}\leftrightarrow 𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}$$
7	2 6	bitri	$$⊢A\in {\mathrm{Fin}}^{\mathrm{III}}\leftrightarrow 𝒫A\in {\mathrm{Fin}}^{\mathrm{IV}}$$