isfin3

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

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

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

Metamath Proof Explorer