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

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 ( 𝐴 ∈ Fin ↔ 𝒫 𝒫 𝐴 ∈ FinIV )

Proof

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