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 e. Fin <-> ~P ~P A e. Fin4 )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. Fin -> A e. _V )
2 elex 
 |-  ( ~P ~P A e. Fin4 -> ~P ~P A e. _V )
3 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
4 pwexb 
 |-  ( ~P A e. _V <-> ~P ~P A e. _V )
5 3 4 bitri 
 |-  ( A e. _V <-> ~P ~P A e. _V )
6 2 5 sylibr 
 |-  ( ~P ~P A e. Fin4 -> A e. _V )
7 ominf 
 |-  -. _om e. Fin
8 pwfi 
 |-  ( A e. Fin <-> ~P A e. Fin )
9 pwfi 
 |-  ( ~P A e. Fin <-> ~P ~P A e. Fin )
10 8 9 bitri 
 |-  ( A e. Fin <-> ~P ~P A e. Fin )
11 domfi 
 |-  ( ( ~P ~P A e. Fin /\ _om ~<_ ~P ~P A ) -> _om e. Fin )
12 11 expcom 
 |-  ( _om ~<_ ~P ~P A -> ( ~P ~P A e. Fin -> _om e. Fin ) )
13 10 12 syl5bi 
 |-  ( _om ~<_ ~P ~P A -> ( A e. Fin -> _om e. Fin ) )
14 7 13 mtoi 
 |-  ( _om ~<_ ~P ~P A -> -. A e. Fin )
15 fineqvlem 
 |-  ( ( A e. _V /\ -. A e. Fin ) -> _om ~<_ ~P ~P A )
16 15 ex 
 |-  ( A e. _V -> ( -. A e. Fin -> _om ~<_ ~P ~P A ) )
17 14 16 impbid2 
 |-  ( A e. _V -> ( _om ~<_ ~P ~P A <-> -. A e. Fin ) )
18 17 con2bid 
 |-  ( A e. _V -> ( A e. Fin <-> -. _om ~<_ ~P ~P A ) )
19 isfin4-2 
 |-  ( ~P ~P A e. _V -> ( ~P ~P A e. Fin4 <-> -. _om ~<_ ~P ~P A ) )
20 5 19 sylbi 
 |-  ( A e. _V -> ( ~P ~P A e. Fin4 <-> -. _om ~<_ ~P ~P A ) )
21 18 20 bitr4d 
 |-  ( A e. _V -> ( A e. Fin <-> ~P ~P A e. Fin4 ) )
22 1 6 21 pm5.21nii 
 |-  ( A e. Fin <-> ~P ~P A e. Fin4 )