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