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 9379

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 9377	. . 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 2108 class class class wbr 5119 Fun wfun 6525 (class class class)co 7405 supp csupp 8159 Fincfn 8959 finSupp cfsupp 9373

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 2007 ax-8 2110 ax-9 2118 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pr 5402

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 2065 df-clab 2714 df-cleq 2727 df-clel 2809 df-rab 3416 df-v 3461 df-dif 3929 df-un 3931 df-ss 3943 df-nul 4309 df-if 4501 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-br 5120 df-opab 5182 df-rel 5661 df-cnv 5662 df-co 5663 df-iota 6484 df-fun 6533 df-fv 6539 df-ov 7408 df-fsupp 9374

This theorem is referenced by: fidmfisupp 9384 finnzfsuppd 9385 suppeqfsuppbi 9391 suppssfifsupp 9392 fsuppunbi 9401 0fsupp 9402 snopfsupp 9403 fsuppres 9405 resfsupp 9408 ffsuppbi 9410 sniffsupp 9412 fsuppco 9414 cantnfp1lem1 9692 fcdmnn0fsuppg 12561 mptnn0fsupp 14015 dprdfadd 20003 lcomfsupp 20859 frlmbas 21715 frlmphllem 21740 frlmsslsp 21756 mplsubglem2 21961 ltbwe 22002 pmatcollpw2lem 22715 rrxmval 25357 offinsupp1 32704 elrspunidl 33443 eulerpartgbij 34404 pwfi2f1o 43120 cantnfub 43345 lcoc0 48398

W3C validator