Theorem pwssfi

Description: Every element of the power set of A is finite if and only if A is finite. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pwssfi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ⊆ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
2		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ∈ Fin )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ∈ Fin )
4	3	ralrimiva	⊢ ( 𝐴 ∈ Fin → ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin )
5		dfss3	⊢ ( 𝒫 𝐴 ⊆ Fin ↔ ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin )
6	4 5	sylibr	⊢ ( 𝐴 ∈ Fin → 𝒫 𝐴 ⊆ Fin )
7		pwidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴 )
8	5	biimpi	⊢ ( 𝒫 𝐴 ⊆ Fin → ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin )
9		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ Fin ↔ 𝐴 ∈ Fin ) )
10	9	rspcva	⊢ ( ( 𝐴 ∈ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin ) → 𝐴 ∈ Fin )
11	7 8 10	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ⊆ Fin ) → 𝐴 ∈ Fin )
12	11	ex	⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ⊆ Fin → 𝐴 ∈ Fin ) )
13	6 12	impbid2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ⊆ Fin ) )