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		simpl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝐴 ∈ Fin )
2		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
3	2	adantl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ⊆ 𝐴 )
4		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ∈ Fin )
5	1 3 4	syl2anc	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ∈ 𝒫 𝐴 ) → 𝑥 ∈ Fin )
6	5	ralrimiva	⊢ ( 𝐴 ∈ Fin → ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin )
7		dfss3	⊢ ( 𝒫 𝐴 ⊆ Fin ↔ ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin )
8	6 7	sylibr	⊢ ( 𝐴 ∈ Fin → 𝒫 𝐴 ⊆ Fin )
9	8	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin → 𝒫 𝐴 ⊆ Fin ) )
10		pwidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴 )
11	10	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ⊆ Fin ) → 𝐴 ∈ 𝒫 𝐴 )
12	7	biimpi	⊢ ( 𝒫 𝐴 ⊆ Fin → ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin )
13	12	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ⊆ Fin ) → ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin )
14		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ Fin ↔ 𝐴 ∈ Fin ) )
15	14	rspcva	⊢ ( ( 𝐴 ∈ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 𝑥 ∈ Fin ) → 𝐴 ∈ Fin )
16	11 13 15	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝒫 𝐴 ⊆ Fin ) → 𝐴 ∈ Fin )
17	16	ex	⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 𝐴 ⊆ Fin → 𝐴 ∈ Fin ) )
18	9 17	impbid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ⊆ Fin ) )