Theorem isfsuppd 9365

Description: Deduction form of isfsupp 9364. (Contributed by SN, 29-Jul-2024.)

Hypotheses

Ref	Expression
isfsuppd.r	⊢ (𝜑 → 𝑅 ∈ 𝑉)
isfsuppd.z	⊢ (𝜑 → 𝑍 ∈ 𝑊)
isfsuppd.1	⊢ (𝜑 → Fun 𝑅)
isfsuppd.2	⊢ (𝜑 → (𝑅 supp 𝑍) ∈ Fin)

Assertion

Ref	Expression
isfsuppd	⊢ (𝜑 → 𝑅 finSupp 𝑍)

Proof of Theorem isfsuppd

Step	Hyp	Ref	Expression
1		isfsuppd.1	. 2 ⊢ (𝜑 → Fun 𝑅)
2		isfsuppd.2	. 2 ⊢ (𝜑 → (𝑅 supp 𝑍) ∈ Fin)
3		isfsuppd.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
4		isfsuppd.z	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝑊)
5		isfsupp 9364	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
6	3, 4, 5	syl2anc 596	. 2 ⊢ (𝜑 → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
7	1, 2, 6	mpbir2and 726	1 ⊢ (𝜑 → 𝑅 finSupp 𝑍)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  Fun wfun 6537  (class class class)co 7424   supp csupp 8183  Fincfn 8980   finSupp cfsupp 9360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-rel 5658  df-cnv 5659  df-co 5660  df-iota 6497  df-fun 6545  df-fv 6551  df-ov 7427  df-fsupp 9361

This theorem is used by:  fczfsuppd  9385  selvvvval  22460  mhpmulcl  22479  psdmplcl  22492  mptiffisupp  33337  indfsd  33485  elrgspnlem2  33854  elrgspnlem4  33856  elrgspnsubrunlem1  33858  elrgspnsubrunlem2  33859  elrspunidl  34028  elrspunsn  34029  extvfvcl  34218  mplmulmvr  34221  psrmonprod  34234  evlselvlem  43725  evlselv  43726