Theorem fdmfifsupp 9345

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 6717	. 2 ⊢ (𝜑 → Fun 𝐹)
3		fdmfisuppfi.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ Fin)
4		fdmfisuppfi.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
5	1, 3, 4	fdmfisuppfi 9344	. 2 ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
6	1	ffnd 6713	. . . 4 ⊢ (𝜑 → 𝐹 Fn 𝐷)
7		fnex 7222	. . . 4 ⊢ ((𝐹 Fn 𝐷 ∧ 𝐷 ∈ Fin) → 𝐹 ∈ V)
8	6, 3, 7	syl2anc 596	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
9		isfsupp 9335	. . 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 2146  Vcvv 3458   class class class wbr 5114  Fun wfun 6537   Fn wfn 6538  ⟶wf 6539  (class class class)co 7423   supp csupp 8165  Fincfn 8952   finSupp cfsupp 9331

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-supp 8166  df-1o 8462  df-en 8953  df-fin 8956  df-fsupp 9332

This theorem is used by:  fsuppmptdm  9346  fndmfifsupp  9348  gsumreidx  20018  gsummptfif1o  20069  gsumle  20246  frlmfibas  21949  elfilspd  21990  rhmpsrlem1  22127  tmdgsum  24289  tsmslem1  24323  tsmssubm  24337  tsmsres  24338  tsmsf1o  24339  tsmsmhm  24340  tsmsadd  24341  tsmsxplem1  24347  tsmsxplem2  24348  imasdsf1olem  24567  xrge0gsumle  25028  xrge0tsms  25029  rrxbasefi  25606  ehlbase  25611  jensenlem2  27189  jensen  27190  amgmlem  27191  amgm  27192  wilthlem2  27270  wilthlem3  27271  wrdfsupp  33294  gsummulsubdishift2  33420  xrge0tsmsd  33424  linds2eq  33725  elrspunidl  33767  rprmdvdsprod  33855  selvply1rhmlema  33939  selvply1rhmlemb  33940  psrmonprod  33973  esplyfvaln  33995  esumpfinvalf  34497  k0004ss2  44918  sge0tsms  47134  fsuppmptdmf  49198  linccl  49234  lcosn0  49240  islinindfis  49269  snlindsntor  49291  ldepspr  49293  zlmodzxzldeplem2  49321  amgmwlem  50690  amgmlemALT  50691