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 ⊢ φ → I ∈ V
sniffsupp.0 ⊢ φ → 0 ˙ ∈ W
sniffsupp.f ⊢ F = x ∈ I ⟼ if x = X A 0 ˙
Assertion sniffsupp ⊢ φ → finSupp 0 ˙⁡ F

Proof

Step Hyp Ref Expression
1 sniffsupp.i ⊢ φ → I ∈ V
2 sniffsupp.0 ⊢ φ → 0 ˙ ∈ W
3 sniffsupp.f ⊢ F = x ∈ I ⟼ if x = X A 0 ˙
4 snfi ⊢ X ∈ Fin
5 eldifsni ⊢ x ∈ I ∖ X → x ≠ X
6 5 adantl ⊢ φ ∧ x ∈ I ∖ X → x ≠ X
7 6 neneqd ⊢ φ ∧ x ∈ I ∖ X → ¬ x = X
8 7 iffalsed ⊢ φ ∧ x ∈ I ∖ X → if x = X A 0 ˙ = 0 ˙
9 8 1 suppss2 ⊢ φ → x ∈ I ⟼ if x = X A 0 ˙ supp 0 ˙ ⊆ X
10 ssfi ⊢ X ∈ Fin ∧ x ∈ I ⟼ if x = X A 0 ˙ supp 0 ˙ ⊆ X → x ∈ I ⟼ if x = X A 0 ˙ supp 0 ˙ ∈ Fin
11 4 9 10 sylancr ⊢ φ → x ∈ I ⟼ if x = X A 0 ˙ supp 0 ˙ ∈ Fin
12 funmpt ⊢ Fun ⁡ x ∈ I ⟼ if x = X A 0 ˙
13 1 mptexd ⊢ φ → x ∈ I ⟼ if x = X A 0 ˙ ∈ V
14 funisfsupp ⊢ Fun ⁡ x ∈ I ⟼ if x = X A 0 ˙ ∧ x ∈ I ⟼ if x = X A 0 ˙ ∈ V ∧ 0 ˙ ∈ W → finSupp 0 ˙⁡ x ∈ I ⟼ if x = X A 0 ˙ ↔ x ∈ I ⟼ if x = X A 0 ˙ supp 0 ˙ ∈ Fin
15 12 13 2 14 mp3an2i ⊢ φ → finSupp 0 ˙⁡ x ∈ I ⟼ if x = X A 0 ˙ ↔ x ∈ I ⟼ if x = X A 0 ˙ supp 0 ˙ ∈ Fin
16 11 15 mpbird ⊢ φ → finSupp 0 ˙⁡ x ∈ I ⟼ if x = X A 0 ˙
17 3 16 eqbrtrid ⊢ φ → finSupp 0 ˙⁡ F