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