Metamath Proof Explorer

Theorem fsuppmptif

Description: A function mapping an argument to either a value of a finitely supported function or zero is finitely supported. (Contributed by AV, 6-Jun-2019)

Ref Expression
Hypotheses fsuppmptif.f ⊢φ→F:A⟶B
fsuppmptif.a ⊢φ→A∈V
fsuppmptif.z ⊢φ→Z∈W
fsuppmptif.s ⊢φ→finSuppZ⁡F
Assertion fsuppmptif ⊢φ→finSuppZ⁡k∈A⟼ifk∈DF⁡kZ

Proof

Step Hyp Ref Expression
1 fsuppmptif.f ⊢φ→F:A⟶B
2 fsuppmptif.a ⊢φ→A∈V
3 fsuppmptif.z ⊢φ→Z∈W
4 fsuppmptif.s ⊢φ→finSuppZ⁡F
5 fvex ⊢F⁡k∈V
6 3 adantr ⊢φ∧k∈A→Z∈W
7 ifexg ⊢F⁡k∈V∧Z∈W→ifk∈DF⁡kZ∈V
8 5 6 7 sylancr ⊢φ∧k∈A→ifk∈DF⁡kZ∈V
9 8 fmpttd ⊢φ→k∈A⟼ifk∈DF⁡kZ:A⟶V
10 9 ffund ⊢φ→Fun⁡k∈A⟼ifk∈DF⁡kZ
11 4 fsuppimpd ⊢φ→FsuppZ∈Fin
12 ssidd ⊢φ→FsuppZ⊆FsuppZ
13 1 12 2 3 suppssr ⊢φ∧k∈A∖suppZ⁡F→F⁡k=Z
14 13 ifeq1d ⊢φ∧k∈A∖suppZ⁡F→ifk∈DF⁡kZ=ifk∈DZZ
15 ifid ⊢ifk∈DZZ=Z
16 14 15 eqtrdi ⊢φ∧k∈A∖suppZ⁡F→ifk∈DF⁡kZ=Z
17 16 2 suppss2 ⊢φ→k∈A⟼ifk∈DF⁡kZsuppZ⊆FsuppZ
18 11 17 ssfid ⊢φ→k∈A⟼ifk∈DF⁡kZsuppZ∈Fin
19 2 mptexd ⊢φ→k∈A⟼ifk∈DF⁡kZ∈V
20 isfsupp ⊢k∈A⟼ifk∈DF⁡kZ∈V∧Z∈W→finSuppZ⁡k∈A⟼ifk∈DF⁡kZ↔Fun⁡k∈A⟼ifk∈DF⁡kZ∧k∈A⟼ifk∈DF⁡kZsuppZ∈Fin
21 19 3 20 syl2anc ⊢φ→finSuppZ⁡k∈A⟼ifk∈DF⁡kZ↔Fun⁡k∈A⟼ifk∈DF⁡kZ∧k∈A⟼ifk∈DF⁡kZsuppZ∈Fin
22 10 18 21 mpbir2and ⊢φ→finSuppZ⁡k∈A⟼ifk∈DF⁡kZ