Metamath Proof Explorer

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 ⊢ A ∈ V → A ∈ Fin ↔ 𝒫 A ⊆ Fin

Proof

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