| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > suppssfifsupp | Structured version Visualization version GIF version | ||
| Description: If the support of a function is a subset of a finite set, the function is finitely supported. (Contributed by AV, 15-Jul-2019.) |
| Ref | Expression |
|---|---|
| suppssfifsupp | ⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ∧ (𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹)) → 𝐺 finSupp 𝑍) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssfi 9160 | . . 3 ⊢ ((𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹) → (𝐺 supp 𝑍) ∈ Fin) | |
| 2 | 1 | adantl 487 | . 2 ⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ∧ (𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹)) → (𝐺 supp 𝑍) ∈ Fin) |
| 3 | 3ancoma 1115 | . . . 4 ⊢ ((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ↔ (Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) | |
| 4 | 3 | birani 509 | . . 3 ⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ∧ (𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹)) → (Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) |
| 5 | funisfsupp 9330 | . . 3 ⊢ ((Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin)) | |
| 6 | 4, 5 | syl 18 | . 2 ⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ∧ (𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹)) → (𝐺 finSupp 𝑍 ↔ (𝐺 supp 𝑍) ∈ Fin)) |
| 7 | 2, 6 | mpbird 260 | 1 ⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑊) ∧ (𝐹 ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ 𝐹)) → 𝐺 finSupp 𝑍) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∈ wcel 2146 ⊆ wss 3906 class class class wbr 5111 Fun wfun 6534 (class class class)co 7416 supp csupp 8158 Fincfn 8945 finSupp cfsupp 9324 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pr 5406 ax-un 7738 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7419 df-om 7865 df-1o 8455 df-en 8946 df-fin 8949 df-fsupp 9325 |
| This theorem is used by: fsuppsssupp 9344 fsuppsssuppgd 9345 fsfnn0gsumfsffz 20077 mptscmfsupp0 21078 uvcff 21971 uvcresum 21973 frlmup1 21978 psrass1lem 22113 psrlidm 22141 psrridm 22142 psrass1 22143 psrass23l 22146 psrcom 22147 psrass23 22148 mvrcl 22171 mplsubrglem 22183 mplsubrg 22184 mplmon 22216 mplmonmul 22217 mplcoe1 22218 mplcoe5 22221 mplbas2 22223 psrbagev1 22258 evlslem2 22260 evlslem3 22261 evlslem6 22262 psropprmul 22427 coe1mul2 22460 evls1fpws 22559 plypf1 26400 tayl0 26556 fsuppcurry1 33115 fsuppcurry2 33116 gsummptres2 33413 elrgspnlem2 33603 elrgspnlem3 33604 psrmonmul 33980 ply1degltdimlem 34052 fedgmullem1 34059 fedgmullem2 34060 evls1fldgencl 34100 lincresunit2 49291 |
| Copyright terms: Public domain | W3C validator |