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 ( 𝜑𝐹 : 𝐴𝐵 )
fsuppmptif.a ( 𝜑𝐴𝑉 )
fsuppmptif.z ( 𝜑𝑍𝑊 )
fsuppmptif.s ( 𝜑𝐹 finSupp 𝑍 )
Assertion fsuppmptif ( 𝜑 → ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fsuppmptif.f ( 𝜑𝐹 : 𝐴𝐵 )
2 fsuppmptif.a ( 𝜑𝐴𝑉 )
3 fsuppmptif.z ( 𝜑𝑍𝑊 )
4 fsuppmptif.s ( 𝜑𝐹 finSupp 𝑍 )
5 fvex ( 𝐹𝑘 ) ∈ V
6 3 adantr ( ( 𝜑𝑘𝐴 ) → 𝑍𝑊 )
7 ifexg ( ( ( 𝐹𝑘 ) ∈ V ∧ 𝑍𝑊 ) → if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ∈ V )
8 5 6 7 sylancr ( ( 𝜑𝑘𝐴 ) → if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ∈ V )
9 8 fmpttd ( 𝜑 → ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) : 𝐴 ⟶ V )
10 9 ffund ( 𝜑 → Fun ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) )
11 4 fsuppimpd ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
12 ssidd ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )
13 1 12 2 3 suppssr ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( 𝐹𝑘 ) = 𝑍 )
14 13 ifeq1d ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) = if ( 𝑘𝐷 , 𝑍 , 𝑍 ) )
15 ifid if ( 𝑘𝐷 , 𝑍 , 𝑍 ) = 𝑍
16 14 15 eqtrdi ( ( 𝜑𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) = 𝑍 )
17 16 2 suppss2 ( 𝜑 → ( ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )
18 11 17 ssfid ( 𝜑 → ( ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) supp 𝑍 ) ∈ Fin )
19 2 mptexd ( 𝜑 → ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) ∈ V )
20 isfsupp ( ( ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) ∈ V ∧ 𝑍𝑊 ) → ( ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) finSupp 𝑍 ↔ ( Fun ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) ∧ ( ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) supp 𝑍 ) ∈ Fin ) ) )
21 19 3 20 syl2anc ( 𝜑 → ( ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) finSupp 𝑍 ↔ ( Fun ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) ∧ ( ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) supp 𝑍 ) ∈ Fin ) ) )
22 10 18 21 mpbir2and ( 𝜑 → ( 𝑘𝐴 ↦ if ( 𝑘𝐷 , ( 𝐹𝑘 ) , 𝑍 ) ) finSupp 𝑍 )