This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )