Theorem fdmfifsupp 9394

Description: A function with a finite domain is always finitely supported. (Contributed by AV, 25-May-2019.)

Hypotheses

Ref	Expression
fdmfisuppfi.f	⊢ (𝜑 → 𝐹:𝐷⟶𝑅)
fdmfisuppfi.d	⊢ (𝜑 → 𝐷 ∈ Fin)
fdmfisuppfi.z	⊢ (𝜑 → 𝑍 ∈ 𝑉)

Assertion

Ref	Expression
fdmfifsupp	⊢ (𝜑 → 𝐹 finSupp 𝑍)

Proof of Theorem fdmfifsupp

Step	Hyp	Ref	Expression
1		fdmfisuppfi.f	. . 3 ⊢ (𝜑 → 𝐹:𝐷⟶𝑅)
2	1	ffund 6736	. 2 ⊢ (𝜑 → Fun 𝐹)
3		fdmfisuppfi.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ Fin)
4		fdmfisuppfi.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
5	1, 3, 4	fdmfisuppfi 9393	. 2 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
6	1	ffnd 6732	. . . 4 ⊢ (𝜑 → 𝐹 Fn 𝐷)
7		fnex 7246	. . . 4 ⊢ ((𝐹 Fn 𝐷 ∧ 𝐷 ∈ Fin) → 𝐹 ∈ V)
8	6, 3, 7	syl2anc 596	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
9		isfsupp 9385	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ 𝑉) → (𝐹 finSupp 𝑍 ↔ (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin)))
10	8, 4, 9	syl2anc 596	. 2 ⊢ (𝜑 → (𝐹 finSupp 𝑍 ↔ (Fun 𝐹 ∧ (𝐹 supp 𝑍) ∈ Fin)))
11	2, 5, 10	mpbir2and 726	1 ⊢ (𝜑 → 𝐹 finSupp 𝑍)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  Vcvv 3454   class class class wbr 5106  Fun wfun 6552   Fn wfn 6553  ⟶wf 6554  (class class class)co 7443   supp csupp 8204  Fincfn 9001   finSupp cfsupp 9381

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-om 7902  df-supp 8205  df-1o 8504  df-en 9002  df-fin 9005  df-fsupp 9382

This theorem is used by:  fsuppmptdm  9395  fndmfifsupp  9397  gsumreidx  20161  gsummptfif1o  20212  gsumle  20389  frlmfibas  22098  elfilspd  22139  rhmpsrlem1  22278  tmdgsum  24444  tsmslem1  24478  tsmssubm  24492  tsmsres  24493  tsmsf1o  24494  tsmsmhm  24495  tsmsadd  24496  tsmsxplem1  24502  tsmsxplem2  24503  imasdsf1olem  24722  xrge0gsumle  25183  xrge0tsms  25184  rrxbasefi  25761  ehlbase  25766  jensenlem2  27345  jensen  27346  amgmlem  27347  amgm  27348  wilthlem2  27426  wilthlem3  27427  mptiffisupp  33357  wrdfsupp  33574  gsummulsubdishift2  33700  xrge0tsmsd  33704  linds2eq  34006  elrspunidl  34048  rprmdvdsprod  34136  evl1deg2  34179  0mplrim  34216  selvply1rhmlema  34220  selvply1rhmlemb  34221  psrmonprod  34254  esplylem  34268  esplyfv1  34271  esplyfvaln  34276  esplyind  34277  esumpfinvalf  34778  k0004ss2  45344  rrxtopnfi  47502  sge0tsms  47595  fsuppmptdmf  49695  linccl  49731  lcosn0  49737  islinindfis  49766  snlindsntor  49788  ldepspr  49790  zlmodzxzldeplem2  49818  amgmwlem  51267  amgmlemALT  51268