Theorem isfsupp 9322

Description: The property of a class to be a finitely supported function (in relation to a given zero). (Contributed by AV, 23-May-2019.)

Assertion

Ref	Expression
isfsupp	⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))

Proof of Theorem isfsupp

Dummy variables 𝑟 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funeq 6538	. . . 4 ⊢ (𝑟 = 𝑅 → (Fun 𝑟 ↔ Fun 𝑅))
2	1	adantr 480	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → (Fun 𝑟 ↔ Fun 𝑅))
3		oveq12 7398	. . . 4 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → (𝑟 supp 𝑧) = (𝑅 supp 𝑍))
4	3	eleq1d 2814	. . 3 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → ((𝑟 supp 𝑧) ∈ Fin ↔ (𝑅 supp 𝑍) ∈ Fin))
5	2, 4	anbi12d 632	. 2 ⊢ ((𝑟 = 𝑅 ∧ 𝑧 = 𝑍) → ((Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin) ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
6		df-fsupp 9319	. 2 ⊢ finSupp = {⟨𝑟, 𝑧⟩ ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)}
7	5, 6	brabga 5496	1 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   class class class wbr 5109  Fun wfun 6507  (class class class)co 7389   supp csupp 8141  Fincfn 8920   finSupp cfsupp 9318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-rel 5647  df-cnv 5648  df-co 5649  df-iota 6466  df-fun 6515  df-fv 6521  df-ov 7392  df-fsupp 9319

This theorem is referenced by:  isfsuppd  9323  funisfsupp  9324  fsuppimp  9325  fdmfifsupp  9332  fczfsuppd  9343  fsuppmptif  9356  fsuppco2  9360  fsuppcor  9361  mndpfsupp  18700  gsumzadd  19858  gsumpt  19898  gsum2dlem2  19907  gsum2d  19908  gsum2d2lem  19909  mhpmulcl  22042  rmfsupp2  33195  elrspunidl  33405  naddcnff  43344  rmfsupp  48351  scmfsupp  48353  mptcfsupp  48355