Metamath Proof Explorer

Theorem pwfilem

Description: Lemma for pwfi . (Contributed by NM, 26-Mar-2007) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 pwfilem.1 ⊢F=c∈𝒫b⟼c∪x
2 pwundif ⊢𝒫b∪x=𝒫b∪x∖𝒫b∪𝒫b
3 1 funmpt2 ⊢Fun⁡F
4 vex ⊢c∈V
5 vsnex ⊢x∈V
6 4 5 unex ⊢c∪x∈V
7 6 1 dmmpti ⊢dom⁡F=𝒫b
8 7 imaeq2i ⊢Fdom⁡F=F𝒫b
9 imadmrn ⊢Fdom⁡F=ran⁡F
10 8 9 eqtr3i ⊢F𝒫b=ran⁡F
11 imafi ⊢Fun⁡F∧𝒫b∈Fin→F𝒫b∈Fin
12 10 11 eqeltrrid ⊢Fun⁡F∧𝒫b∈Fin→ran⁡F∈Fin
13 3 12 mpan ⊢𝒫b∈Fin→ran⁡F∈Fin
14 eldifi ⊢d∈𝒫b∪x∖𝒫b→d∈𝒫b∪x
15 5 elpwun ⊢d∈𝒫b∪x↔d∖x∈𝒫b
16 14 15 sylib ⊢d∈𝒫b∪x∖𝒫b→d∖x∈𝒫b
17 undif1 ⊢d∖x∪x=d∪x
18 elpwunsn ⊢d∈𝒫b∪x∖𝒫b→x∈d
19 18 snssd ⊢d∈𝒫b∪x∖𝒫b→x⊆d
20 ssequn2 ⊢x⊆d↔d∪x=d
21 19 20 sylib ⊢d∈𝒫b∪x∖𝒫b→d∪x=d
22 17 21 eqtr2id ⊢d∈𝒫b∪x∖𝒫b→d=d∖x∪x
23 uneq1 ⊢c=d∖x→c∪x=d∖x∪x
24 23 rspceeqv ⊢d∖x∈𝒫b∧d=d∖x∪x→∃c∈𝒫bd=c∪x
25 16 22 24 syl2anc ⊢d∈𝒫b∪x∖𝒫b→∃c∈𝒫bd=c∪x
26 1 25 14 elrnmptd ⊢d∈𝒫b∪x∖𝒫b→d∈ran⁡F
27 26 ssriv ⊢𝒫b∪x∖𝒫b⊆ran⁡F
28 ssfi ⊢ran⁡F∈Fin∧𝒫b∪x∖𝒫b⊆ran⁡F→𝒫b∪x∖𝒫b∈Fin
29 13 27 28 sylancl ⊢𝒫b∈Fin→𝒫b∪x∖𝒫b∈Fin
30 unfi ⊢𝒫b∪x∖𝒫b∈Fin∧𝒫b∈Fin→𝒫b∪x∖𝒫b∪𝒫b∈Fin
31 29 30 mpancom ⊢𝒫b∈Fin→𝒫b∪x∖𝒫b∪𝒫b∈Fin
32 2 31 eqeltrid ⊢𝒫b∈Fin→𝒫b∪x∈Fin