Metamath Proof Explorer


Theorem pwfiOLD

Description: Obsolete version of pwfi as of 7-Sep-2024. (Contributed by NM, 26-Mar-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pwfiOLD
|- ( A e. Fin <-> ~P A e. Fin )

Proof

Step Hyp Ref Expression
1 isfi
 |-  ( A e. Fin <-> E. m e. _om A ~~ m )
2 pweq
 |-  ( m = (/) -> ~P m = ~P (/) )
3 2 eleq1d
 |-  ( m = (/) -> ( ~P m e. Fin <-> ~P (/) e. Fin ) )
4 pweq
 |-  ( m = k -> ~P m = ~P k )
5 4 eleq1d
 |-  ( m = k -> ( ~P m e. Fin <-> ~P k e. Fin ) )
6 pweq
 |-  ( m = suc k -> ~P m = ~P suc k )
7 df-suc
 |-  suc k = ( k u. { k } )
8 7 pweqi
 |-  ~P suc k = ~P ( k u. { k } )
9 6 8 eqtrdi
 |-  ( m = suc k -> ~P m = ~P ( k u. { k } ) )
10 9 eleq1d
 |-  ( m = suc k -> ( ~P m e. Fin <-> ~P ( k u. { k } ) e. Fin ) )
11 pw0
 |-  ~P (/) = { (/) }
12 df1o2
 |-  1o = { (/) }
13 11 12 eqtr4i
 |-  ~P (/) = 1o
14 1onn
 |-  1o e. _om
15 ssid
 |-  1o C_ 1o
16 ssnnfi
 |-  ( ( 1o e. _om /\ 1o C_ 1o ) -> 1o e. Fin )
17 14 15 16 mp2an
 |-  1o e. Fin
18 13 17 eqeltri
 |-  ~P (/) e. Fin
19 eqid
 |-  ( c e. ~P k |-> ( c u. { k } ) ) = ( c e. ~P k |-> ( c u. { k } ) )
20 19 pwfilem
 |-  ( ~P k e. Fin -> ~P ( k u. { k } ) e. Fin )
21 20 a1i
 |-  ( k e. _om -> ( ~P k e. Fin -> ~P ( k u. { k } ) e. Fin ) )
22 3 5 10 18 21 finds1
 |-  ( m e. _om -> ~P m e. Fin )
23 pwen
 |-  ( A ~~ m -> ~P A ~~ ~P m )
24 enfii
 |-  ( ( ~P m e. Fin /\ ~P A ~~ ~P m ) -> ~P A e. Fin )
25 22 23 24 syl2an
 |-  ( ( m e. _om /\ A ~~ m ) -> ~P A e. Fin )
26 25 rexlimiva
 |-  ( E. m e. _om A ~~ m -> ~P A e. Fin )
27 1 26 sylbi
 |-  ( A e. Fin -> ~P A e. Fin )
28 pwexr
 |-  ( ~P A e. Fin -> A e. _V )
29 canth2g
 |-  ( A e. _V -> A ~< ~P A )
30 sdomdom
 |-  ( A ~< ~P A -> A ~<_ ~P A )
31 28 29 30 3syl
 |-  ( ~P A e. Fin -> A ~<_ ~P A )
32 domfi
 |-  ( ( ~P A e. Fin /\ A ~<_ ~P A ) -> A e. Fin )
33 31 32 mpdan
 |-  ( ~P A e. Fin -> A e. Fin )
34 27 33 impbii
 |-  ( A e. Fin <-> ~P A e. Fin )