Metamath Proof Explorer

Theorem pwfilemOLD

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

Ref Expression
Hypothesis pwfilemOLD.1 ⊢F=c∈𝒫b⟼c∪x
Assertion pwfilemOLD ⊢𝒫b∈Fin→𝒫b∪x∈Fin

Proof

Step Hyp Ref Expression
1 pwfilemOLD.1 ⊢F=c∈𝒫b⟼c∪x
2 pwundif ⊢𝒫b∪x=𝒫b∪x∖𝒫b∪𝒫b
3 vex ⊢c∈V
4 snex ⊢x∈V
5 3 4 unex ⊢c∪x∈V
6 5 1 fnmpti ⊢FFn𝒫b
7 dffn4 ⊢FFn𝒫b↔F:𝒫b⟶ontoran⁡F
8 6 7 mpbi ⊢F:𝒫b⟶ontoran⁡F
9 fodomfi ⊢𝒫b∈Fin∧F:𝒫b⟶ontoran⁡F→ran⁡F≼𝒫b
10 8 9 mpan2 ⊢𝒫b∈Fin→ran⁡F≼𝒫b
11 domfi ⊢𝒫b∈Fin∧ran⁡F≼𝒫b→ran⁡F∈Fin
12 10 11 mpdan ⊢𝒫b∈Fin→ran⁡F∈Fin
13 eldifi ⊢d∈𝒫b∪x∖𝒫b→d∈𝒫b∪x
14 4 elpwun ⊢d∈𝒫b∪x↔d∖x∈𝒫b
15 13 14 sylib ⊢d∈𝒫b∪x∖𝒫b→d∖x∈𝒫b
16 undif1 ⊢d∖x∪x=d∪x
17 elpwunsn ⊢d∈𝒫b∪x∖𝒫b→x∈d
18 17 snssd ⊢d∈𝒫b∪x∖𝒫b→x⊆d
19 ssequn2 ⊢x⊆d↔d∪x=d
20 18 19 sylib ⊢d∈𝒫b∪x∖𝒫b→d∪x=d
21 16 20 eqtr2id ⊢d∈𝒫b∪x∖𝒫b→d=d∖x∪x
22 uneq1 ⊢c=d∖x→c∪x=d∖x∪x
23 22 rspceeqv ⊢d∖x∈𝒫b∧d=d∖x∪x→∃c∈𝒫bd=c∪x
24 15 21 23 syl2anc ⊢d∈𝒫b∪x∖𝒫b→∃c∈𝒫bd=c∪x
25 1 5 elrnmpti ⊢d∈ran⁡F↔∃c∈𝒫bd=c∪x
26 24 25 sylibr ⊢d∈𝒫b∪x∖𝒫b→d∈ran⁡F
27 26 ssriv ⊢𝒫b∪x∖𝒫b⊆ran⁡F
28 ssdomg ⊢ran⁡F∈Fin→𝒫b∪x∖𝒫b⊆ran⁡F→𝒫b∪x∖𝒫b≼ran⁡F
29 12 27 28 mpisyl ⊢𝒫b∈Fin→𝒫b∪x∖𝒫b≼ran⁡F
30 domfi ⊢ran⁡F∈Fin∧𝒫b∪x∖𝒫b≼ran⁡F→𝒫b∪x∖𝒫b∈Fin
31 12 29 30 syl2anc ⊢𝒫b∈Fin→𝒫b∪x∖𝒫b∈Fin
32 unfi ⊢𝒫b∪x∖𝒫b∈Fin∧𝒫b∈Fin→𝒫b∪x∖𝒫b∪𝒫b∈Fin
33 31 32 mpancom ⊢𝒫b∈Fin→𝒫b∪x∖𝒫b∪𝒫b∈Fin
34 2 33 eqeltrid ⊢𝒫b∈Fin→𝒫b∪x∈Fin