Theorem sniffsupp

Description: A function mapping all but one arguments to zero is finitely supported. (Contributed by AV, 8-Jul-2019)

	Ref	Expression
Hypotheses	sniffsupp.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	sniffsupp.0	⊢ ( 𝜑 → 0 ∈ 𝑊 )
	sniffsupp.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) )
Assertion	sniffsupp	⊢ ( 𝜑 → 𝐹 finSupp 0 )

Proof

Step	Hyp	Ref	Expression
1		sniffsupp.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
2		sniffsupp.0	⊢ ( 𝜑 → 0 ∈ 𝑊 )
3		sniffsupp.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) )
4		snfi	⊢ { 𝑋 } ∈ Fin
5		eldifsni	⊢ ( 𝑥 ∈ ( 𝐼 ∖ { 𝑋 } ) → 𝑥 ≠ 𝑋 )
6	5	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → 𝑥 ≠ 𝑋 )
7	6	neneqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → ¬ 𝑥 = 𝑋 )
8	7	iffalsed	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → if ( 𝑥 = 𝑋 , 𝐴 , 0 ) = 0 )
9	8 1	suppss2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ⊆ { 𝑋 } )
10		ssfi	⊢ ( ( { 𝑋 } ∈ Fin ∧ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ⊆ { 𝑋 } ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ∈ Fin )
11	4 9 10	sylancr	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ∈ Fin )
12		funmpt	⊢ Fun ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) )
13	1	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ∈ V )
14		funisfsupp	⊢ ( ( Fun ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ∧ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ∈ V ∧ 0 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ∈ Fin ) )
15	12 13 2 14	mp3an2i	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) finSupp 0 ↔ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ∈ Fin ) )
16	11 15	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) finSupp 0 )
17	3 16	eqbrtrid	⊢ ( 𝜑 → 𝐹 finSupp 0 )