This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 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 ) )