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 9270

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 9268	. . 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 2113 class class class wbr 5098 Fun wfun 6486 (class class class)co 7358 supp csupp 8102 Fincfn 8883 finSupp cfsupp 9264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-rel 5631 df-cnv 5632 df-co 5633 df-iota 6448 df-fun 6494 df-fv 6500 df-ov 7361 df-fsupp 9265

This theorem is referenced by: fidmfisupp 9275 finnzfsuppd 9276 suppeqfsuppbi 9282 suppssfifsupp 9283 fsuppunbi 9292 0fsupp 9293 snopfsupp 9294 fsuppres 9296 resfsupp 9299 ffsuppbi 9301 sniffsupp 9303 fsuppco 9305 cantnfp1lem1 9587 fcdmnn0fsuppg 12461 mptnn0fsupp 13920 dprdfadd 19951 lcomfsupp 20853 frlmbas 21710 frlmphllem 21735 frlmsslsp 21751 mplsubglem2 21956 ltbwe 21999 pmatcollpw2lem 22721 rrxmval 25361 offinsupp1 32805 elrspunidl 33509 eulerpartgbij 34529 pwfi2f1o 43338 cantnfub 43563 lcoc0 48668

W3C validator