Metamath Proof Explorer

Theorem isfin1-2

Description: A set is finite in the usual sense iff the power set of its power set is Dedekind finite. (Contributed by Stefan O'Rear, 3-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion isfin1-2 ⊢ A ∈ Fin ↔ 𝒫 𝒫 A ∈ FinIV

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ Fin → A ∈ V
2 elex ⊢ 𝒫 𝒫 A ∈ FinIV → 𝒫 𝒫 A ∈ V
3 pwexb ⊢ A ∈ V ↔ 𝒫 A ∈ V
4 pwexb ⊢ 𝒫 A ∈ V ↔ 𝒫 𝒫 A ∈ V
5 3 4 bitri ⊢ A ∈ V ↔ 𝒫 𝒫 A ∈ V
6 2 5 sylibr ⊢ 𝒫 𝒫 A ∈ FinIV → A ∈ V
7 ominf ⊢ ¬ ω ∈ Fin
8 pwfi ⊢ A ∈ Fin ↔ 𝒫 A ∈ Fin
9 pwfi ⊢ 𝒫 A ∈ Fin ↔ 𝒫 𝒫 A ∈ Fin
10 8 9 bitri ⊢ A ∈ Fin ↔ 𝒫 𝒫 A ∈ Fin
11 domfi ⊢ 𝒫 𝒫 A ∈ Fin ∧ ω ≼ 𝒫 𝒫 A → ω ∈ Fin
12 11 expcom ⊢ ω ≼ 𝒫 𝒫 A → 𝒫 𝒫 A ∈ Fin → ω ∈ Fin
13 10 12 syl5bi ⊢ ω ≼ 𝒫 𝒫 A → A ∈ Fin → ω ∈ Fin
14 7 13 mtoi ⊢ ω ≼ 𝒫 𝒫 A → ¬ A ∈ Fin
15 fineqvlem ⊢ A ∈ V ∧ ¬ A ∈ Fin → ω ≼ 𝒫 𝒫 A
16 15 ex ⊢ A ∈ V → ¬ A ∈ Fin → ω ≼ 𝒫 𝒫 A
17 14 16 impbid2 ⊢ A ∈ V → ω ≼ 𝒫 𝒫 A ↔ ¬ A ∈ Fin
18 17 con2bid ⊢ A ∈ V → A ∈ Fin ↔ ¬ ω ≼ 𝒫 𝒫 A
19 isfin4-2 ⊢ 𝒫 𝒫 A ∈ V → 𝒫 𝒫 A ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝒫 A
20 5 19 sylbi ⊢ A ∈ V → 𝒫 𝒫 A ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝒫 A
21 18 20 bitr4d ⊢ A ∈ V → A ∈ Fin ↔ 𝒫 𝒫 A ∈ FinIV
22 1 6 21 pm5.21nii ⊢ A ∈ Fin ↔ 𝒫 𝒫 A ∈ FinIV