![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > suppss | Structured version Visualization version GIF version |
Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
Ref | Expression |
---|---|
suppss.f | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
suppss.n | ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑘) = 𝑍) |
Ref | Expression |
---|---|
suppss | ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suppss.f | . . . . . . . 8 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | 1 | ffnd 6383 | . . . . . . 7 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
3 | 2 | adantl 482 | . . . . . 6 ⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝐹 Fn 𝐴) |
4 | fdm 6390 | . . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
5 | dmexg 7469 | . . . . . . . . . 10 ⊢ (𝐹 ∈ V → dom 𝐹 ∈ V) | |
6 | 5 | adantr 481 | . . . . . . . . 9 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → dom 𝐹 ∈ V) |
7 | eleq1 2870 | . . . . . . . . . 10 ⊢ (𝐴 = dom 𝐹 → (𝐴 ∈ V ↔ dom 𝐹 ∈ V)) | |
8 | 7 | eqcoms 2803 | . . . . . . . . 9 ⊢ (dom 𝐹 = 𝐴 → (𝐴 ∈ V ↔ dom 𝐹 ∈ V)) |
9 | 6, 8 | syl5ibr 247 | . . . . . . . 8 ⊢ (dom 𝐹 = 𝐴 → ((𝐹 ∈ V ∧ 𝑍 ∈ V) → 𝐴 ∈ V)) |
10 | 1, 4, 9 | 3syl 18 | . . . . . . 7 ⊢ (𝜑 → ((𝐹 ∈ V ∧ 𝑍 ∈ V) → 𝐴 ∈ V)) |
11 | 10 | impcom 408 | . . . . . 6 ⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝐴 ∈ V) |
12 | simplr 765 | . . . . . 6 ⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → 𝑍 ∈ V) | |
13 | elsuppfn 7689 | . . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 𝑍 ∈ V) → (𝑘 ∈ (𝐹 supp 𝑍) ↔ (𝑘 ∈ 𝐴 ∧ (𝐹‘𝑘) ≠ 𝑍))) | |
14 | 3, 11, 12, 13 | syl3anc 1364 | . . . . 5 ⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝑘 ∈ (𝐹 supp 𝑍) ↔ (𝑘 ∈ 𝐴 ∧ (𝐹‘𝑘) ≠ 𝑍))) |
15 | eldif 3869 | . . . . . . . . 9 ⊢ (𝑘 ∈ (𝐴 ∖ 𝑊) ↔ (𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊)) | |
16 | suppss.n | . . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑘) = 𝑍) | |
17 | 16 | adantll 710 | . . . . . . . . 9 ⊢ ((((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑘) = 𝑍) |
18 | 15, 17 | sylan2br 594 | . . . . . . . 8 ⊢ ((((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ (𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊)) → (𝐹‘𝑘) = 𝑍) |
19 | 18 | expr 457 | . . . . . . 7 ⊢ ((((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → (¬ 𝑘 ∈ 𝑊 → (𝐹‘𝑘) = 𝑍)) |
20 | 19 | necon1ad 3001 | . . . . . 6 ⊢ ((((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) ≠ 𝑍 → 𝑘 ∈ 𝑊)) |
21 | 20 | expimpd 454 | . . . . 5 ⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → ((𝑘 ∈ 𝐴 ∧ (𝐹‘𝑘) ≠ 𝑍) → 𝑘 ∈ 𝑊)) |
22 | 14, 21 | sylbid 241 | . . . 4 ⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝑘 ∈ (𝐹 supp 𝑍) → 𝑘 ∈ 𝑊)) |
23 | 22 | ssrdv 3895 | . . 3 ⊢ (((𝐹 ∈ V ∧ 𝑍 ∈ V) ∧ 𝜑) → (𝐹 supp 𝑍) ⊆ 𝑊) |
24 | 23 | ex 413 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)) |
25 | supp0prc 7684 | . . . 4 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) | |
26 | 0ss 4270 | . . . 4 ⊢ ∅ ⊆ 𝑊 | |
27 | 25, 26 | syl6eqss 3942 | . . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ 𝑊) |
28 | 27 | a1d 25 | . 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊)) |
29 | 24, 28 | pm2.61i 183 | 1 ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ≠ wne 2984 Vcvv 3437 ∖ cdif 3856 ⊆ wss 3859 ∅c0 4211 dom cdm 5443 Fn wfn 6220 ⟶wf 6221 ‘cfv 6225 (class class class)co 7016 supp csupp 7681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-supp 7682 |
This theorem is referenced by: suppofssd 7718 fsuppco2 8712 fsuppcor 8713 cantnfp1lem1 8987 cantnfp1lem3 8989 gsumzaddlem 18761 gsumzmhm 18777 gsum2d2lem 18813 lcomfsupp 19364 psrbaglesupp 19836 mplsubglem 19902 mpllsslem 19903 mplsubrglem 19907 mvrcl 19917 evlslem3 19981 mhpvscacl 20024 frlmssuvc1 20620 frlmsslsp 20622 frlmup2 20625 deg1mul3le 24393 jensen 25248 suppovss 30116 fsuppcurry1 30149 fsuppcurry2 30150 resf1o 30154 fedgmullem1 30629 |
Copyright terms: Public domain | W3C validator |