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 )