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 Fin 𝒫 A Fin

Proof

Step Hyp Ref Expression
1 isfi A Fin m ω A m
2 pweq m = 𝒫 m = 𝒫
3 2 eleq1d m = 𝒫 m Fin 𝒫 Fin
4 pweq m = k 𝒫 m = 𝒫 k
5 4 eleq1d m = k 𝒫 m Fin 𝒫 k Fin
6 pweq m = suc k 𝒫 m = 𝒫 suc k
7 df-suc suc k = k k
8 7 pweqi 𝒫 suc k = 𝒫 k k
9 6 8 eqtrdi m = suc k 𝒫 m = 𝒫 k k
10 9 eleq1d m = suc k 𝒫 m Fin 𝒫 k k Fin
11 pw0 𝒫 =
12 df1o2 1 𝑜 =
13 11 12 eqtr4i 𝒫 = 1 𝑜
14 1onn 1 𝑜 ω
15 ssid 1 𝑜 1 𝑜
16 ssnnfi 1 𝑜 ω 1 𝑜 1 𝑜 1 𝑜 Fin
17 14 15 16 mp2an 1 𝑜 Fin
18 13 17 eqeltri 𝒫 Fin
19 eqid c 𝒫 k c k = c 𝒫 k c k
20 19 pwfilem 𝒫 k Fin 𝒫 k k Fin
21 20 a1i k ω 𝒫 k Fin 𝒫 k k Fin
22 3 5 10 18 21 finds1 m ω 𝒫 m Fin
23 pwen A m 𝒫 A 𝒫 m
24 enfii 𝒫 m Fin 𝒫 A 𝒫 m 𝒫 A Fin
25 22 23 24 syl2an m ω A m 𝒫 A Fin
26 25 rexlimiva m ω A m 𝒫 A Fin
27 1 26 sylbi A Fin 𝒫 A Fin
28 pwexr 𝒫 A Fin A V
29 canth2g A V A 𝒫 A
30 sdomdom A 𝒫 A A 𝒫 A
31 28 29 30 3syl 𝒫 A Fin A 𝒫 A
32 domfi 𝒫 A Fin A 𝒫 A A Fin
33 31 32 mpdan 𝒫 A Fin A Fin
34 27 33 impbii A Fin 𝒫 A Fin