Theorem isfin3

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

	Ref	Expression
Assertion	isfin3	⊢ ( 𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV )

Proof

Step	Hyp	Ref	Expression
1		df-fin3	⊢ FinIII = { 𝑥 ∣ 𝒫 𝑥 ∈ FinIV }
2	1	eleq2i	⊢ ( 𝐴 ∈ FinIII ↔ 𝐴 ∈ { 𝑥 ∣ 𝒫 𝑥 ∈ FinIV } )
3		pwexr	⊢ ( 𝒫 𝐴 ∈ FinIV → 𝐴 ∈ V )
4		pweq	⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
5	4	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝒫 𝑥 ∈ FinIV ↔ 𝒫 𝐴 ∈ FinIV ) )
6	3 5	elab3	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝒫 𝑥 ∈ FinIV } ↔ 𝒫 𝐴 ∈ FinIV )
7	2 6	bitri	⊢ ( 𝐴 ∈ FinIII ↔ 𝒫 𝐴 ∈ FinIV )