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 9257

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 9255	. . 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 5092 Fun wfun 6476 (class class class)co 7349 supp csupp 8093 Fincfn 8872 finSupp cfsupp 9251

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 5235 ax-nul 5245 ax-pr 5371

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 3395 df-v 3438 df-dif 3906 df-un 3908 df-ss 3920 df-nul 4285 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-br 5093 df-opab 5155 df-rel 5626 df-cnv 5627 df-co 5628 df-iota 6438 df-fun 6484 df-fv 6490 df-ov 7352 df-fsupp 9252

This theorem is referenced by: fidmfisupp 9262 finnzfsuppd 9263 suppeqfsuppbi 9269 suppssfifsupp 9270 fsuppunbi 9279 0fsupp 9280 snopfsupp 9281 fsuppres 9283 resfsupp 9286 ffsuppbi 9288 sniffsupp 9290 fsuppco 9292 cantnfp1lem1 9574 fcdmnn0fsuppg 12444 mptnn0fsupp 13904 dprdfadd 19901 lcomfsupp 20805 frlmbas 21662 frlmphllem 21687 frlmsslsp 21703 mplsubglem2 21908 ltbwe 21949 pmatcollpw2lem 22662 rrxmval 25303 offinsupp1 32670 elrspunidl 33365 eulerpartgbij 34340 pwfi2f1o 43069 cantnfub 43294 lcoc0 48407

W3C validator