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 ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )

Proof

Step Hyp Ref Expression
1 isfi ( 𝐴 ∈ Fin ↔ ∃ 𝑚 ∈ ω 𝐴𝑚 )
2 pweq ( 𝑚 = ∅ → 𝒫 𝑚 = 𝒫 ∅ )
3 2 eleq1d ( 𝑚 = ∅ → ( 𝒫 𝑚 ∈ Fin ↔ 𝒫 ∅ ∈ Fin ) )
4 pweq ( 𝑚 = 𝑘 → 𝒫 𝑚 = 𝒫 𝑘 )
5 4 eleq1d ( 𝑚 = 𝑘 → ( 𝒫 𝑚 ∈ Fin ↔ 𝒫 𝑘 ∈ Fin ) )
6 pweq ( 𝑚 = suc 𝑘 → 𝒫 𝑚 = 𝒫 suc 𝑘 )
7 df-suc suc 𝑘 = ( 𝑘 ∪ { 𝑘 } )
8 7 pweqi 𝒫 suc 𝑘 = 𝒫 ( 𝑘 ∪ { 𝑘 } )
9 6 8 eqtrdi ( 𝑚 = suc 𝑘 → 𝒫 𝑚 = 𝒫 ( 𝑘 ∪ { 𝑘 } ) )
10 9 eleq1d ( 𝑚 = suc 𝑘 → ( 𝒫 𝑚 ∈ Fin ↔ 𝒫 ( 𝑘 ∪ { 𝑘 } ) ∈ Fin ) )
11 pw0 𝒫 ∅ = { ∅ }
12 df1o2 1o = { ∅ }
13 11 12 eqtr4i 𝒫 ∅ = 1o
14 1onn 1o ∈ ω
15 ssid 1o ⊆ 1o
16 ssnnfi ( ( 1o ∈ ω ∧ 1o ⊆ 1o ) → 1o ∈ Fin )
17 14 15 16 mp2an 1o ∈ Fin
18 13 17 eqeltri 𝒫 ∅ ∈ Fin
19 eqid ( 𝑐 ∈ 𝒫 𝑘 ↦ ( 𝑐 ∪ { 𝑘 } ) ) = ( 𝑐 ∈ 𝒫 𝑘 ↦ ( 𝑐 ∪ { 𝑘 } ) )
20 19 pwfilem ( 𝒫 𝑘 ∈ Fin → 𝒫 ( 𝑘 ∪ { 𝑘 } ) ∈ Fin )
21 20 a1i ( 𝑘 ∈ ω → ( 𝒫 𝑘 ∈ Fin → 𝒫 ( 𝑘 ∪ { 𝑘 } ) ∈ Fin ) )
22 3 5 10 18 21 finds1 ( 𝑚 ∈ ω → 𝒫 𝑚 ∈ Fin )
23 pwen ( 𝐴𝑚 → 𝒫 𝐴 ≈ 𝒫 𝑚 )
24 enfii ( ( 𝒫 𝑚 ∈ Fin ∧ 𝒫 𝐴 ≈ 𝒫 𝑚 ) → 𝒫 𝐴 ∈ Fin )
25 22 23 24 syl2an ( ( 𝑚 ∈ ω ∧ 𝐴𝑚 ) → 𝒫 𝐴 ∈ Fin )
26 25 rexlimiva ( ∃ 𝑚 ∈ ω 𝐴𝑚 → 𝒫 𝐴 ∈ Fin )
27 1 26 sylbi ( 𝐴 ∈ Fin → 𝒫 𝐴 ∈ Fin )
28 pwexr ( 𝒫 𝐴 ∈ Fin → 𝐴 ∈ V )
29 canth2g ( 𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴 )
30 sdomdom ( 𝐴 ≺ 𝒫 𝐴𝐴 ≼ 𝒫 𝐴 )
31 28 29 30 3syl ( 𝒫 𝐴 ∈ Fin → 𝐴 ≼ 𝒫 𝐴 )
32 domfi ( ( 𝒫 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝒫 𝐴 ) → 𝐴 ∈ Fin )
33 31 32 mpdan ( 𝒫 𝐴 ∈ Fin → 𝐴 ∈ Fin )
34 27 33 impbii ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )