funisfsupp - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > funisfsupp		Structured version Visualization version GIF version

Theorem funisfsupp 9318

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

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

**Proof of Theorem funisfsupp**
Step	Hyp	Ref	Expression
1		isfsupp 9316	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
2	1	3adant1 1130	. 2 ⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
3		ibar 528	. . . 4 ⊢ (Fun 𝑅 → ((𝑅 supp 𝑍) ∈ Fin ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
4	3	bicomd 223	. . 3 ⊢ (Fun 𝑅 → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
5	4	3ad2ant1 1133	. 2 ⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
6	2, 5	bitrd 279	1 ⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∈ wcel 2109 class class class wbr 5107 Fun wfun 6505 (class class class)co 7387 supp csupp 8139 Fincfn 8918 finSupp cfsupp 9312

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 2701 ax-sep 5251 ax-nul 5261 ax-pr 5387

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 2708 df-cleq 2721 df-clel 2803 df-rab 3406 df-v 3449 df-dif 3917 df-un 3919 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-br 5108 df-opab 5170 df-rel 5645 df-cnv 5646 df-co 5647 df-iota 6464 df-fun 6513 df-fv 6519 df-ov 7390 df-fsupp 9313

This theorem is referenced by: fidmfisupp 9323 finnzfsuppd 9324 suppeqfsuppbi 9330 suppssfifsupp 9331 fsuppunbi 9340 0fsupp 9341 snopfsupp 9342 fsuppres 9344 resfsupp 9347 ffsuppbi 9349 sniffsupp 9351 fsuppco 9353 cantnfp1lem1 9631 fcdmnn0fsuppg 12502 mptnn0fsupp 13962 dprdfadd 19952 lcomfsupp 20808 frlmbas 21664 frlmphllem 21689 frlmsslsp 21705 mplsubglem2 21910 ltbwe 21951 pmatcollpw2lem 22664 rrxmval 25305 offinsupp1 32650 elrspunidl 33399 eulerpartgbij 34363 pwfi2f1o 43085 cantnfub 43310 lcoc0 48411

W3C validator