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 syl5bi ( ω ≼ 𝒫 𝒫 𝐴 → ( 𝐴 ∈ 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 )