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 9063

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 9062	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
2	1	3adant1 1128	. 2 ⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
3		ibar 528	. . . 4 ⊢ (Fun 𝑅 → ((𝑅 supp 𝑍) ∈ Fin ↔ (Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin)))
4	3	bicomd 222	. . 3 ⊢ (Fun 𝑅 → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
5	4	3ad2ant1 1131	. 2 ⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((Fun 𝑅 ∧ (𝑅 supp 𝑍) ∈ Fin) ↔ (𝑅 supp 𝑍) ∈ Fin))
6	2, 5	bitrd 278	1 ⊢ ((Fun 𝑅 ∧ 𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 finSupp 𝑍 ↔ (𝑅 supp 𝑍) ∈ Fin))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 ∈ wcel 2108 class class class wbr 5070 Fun wfun 6412 (class class class)co 7255 supp csupp 7948 Fincfn 8691 finSupp cfsupp 9058

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-rel 5587 df-cnv 5588 df-co 5589 df-iota 6376 df-fun 6420 df-fv 6426 df-ov 7258 df-fsupp 9059

This theorem is referenced by: suppeqfsuppbi 9072 suppssfifsupp 9073 fsuppunbi 9079 0fsupp 9080 snopfsupp 9081 fsuppres 9083 resfsupp 9085 frnfsuppbi 9087 sniffsupp 9089 fsuppco 9091 cantnfp1lem1 9366 frnnn0fsuppg 12222 mptnn0fsupp 13645 dprdfadd 19538 lcomfsupp 20078 frlmbas 20872 frlmphllem 20897 frlmsslsp 20913 mplsubglem2 21117 ltbwe 21155 pmatcollpw2lem 21834 rrxmval 24474 offinsupp1 30964 elrspunidl 31508 eulerpartgbij 32239 pwfi2f1o 40837 finnzfsuppd 41709 fidmfisupp 42628 lcoc0 45651

W3C validator