![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > suppssdm | Structured version Visualization version GIF version |
Description: The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.) |
Ref | Expression |
---|---|
suppssdm | ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suppval 8150 | . . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}}) | |
2 | ssrab2 4076 | . . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹 | |
3 | 1, 2 | eqsstrdi 4035 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹) |
4 | supp0prc 8151 | . . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) | |
5 | 0ss 4395 | . . 3 ⊢ ∅ ⊆ dom 𝐹 | |
6 | 4, 5 | eqsstrdi 4035 | . 2 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹) |
7 | 3, 6 | pm2.61i 182 | 1 ⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 394 ∈ wcel 2104 ≠ wne 2938 {crab 3430 Vcvv 3472 ⊆ wss 3947 ∅c0 4321 {csn 4627 dom cdm 5675 “ cima 5678 (class class class)co 7411 supp csupp 8148 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7727 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-supp 8149 |
This theorem is referenced by: snopsuppss 8166 wemapso2lem 9549 cantnfcl 9664 cantnfle 9668 cantnflt 9669 cantnff 9671 cantnfres 9674 cantnfp1lem3 9677 cantnflem1b 9683 cantnflem1 9686 cantnflem3 9688 cnfcomlem 9696 cnfcom 9697 cnfcom3lem 9700 cnfcom3 9701 fsuppmapnn0fiublem 13959 fsuppmapnn0fiub 13960 gsumval3lem1 19814 gsumval3lem2 19815 gsumval3 19816 gsumzres 19818 gsumzcl2 19819 gsumzf1o 19821 gsumzaddlem 19830 gsumconst 19843 gsumzoppg 19853 gsum2d 19881 dpjidcl 19969 gsumfsum 21212 regsumsupp 21394 frlmlbs 21571 psrass1lemOLD 21712 psrass1lem 21715 psrass1 21744 psrass23l 21747 psrcom 21748 psrass23 21749 mplcoe1 21811 psropprmul 21980 coe1mul2 22011 tsmsgsum 23863 rrxcph 25140 rrxsuppss 25151 rrxmval 25153 mdegfval 25815 mdegleb 25817 mdegldg 25819 deg1mul3le 25869 wilthlem3 26810 suppovss 32173 fressupp 32177 ressupprn 32179 supppreima 32180 fsupprnfi 32181 fsuppcurry1 32217 fsuppcurry2 32218 gsumhashmul 32478 elrspunidl 32820 fedgmullem1 33002 zarcmplem 33159 fdivmpt 47313 fdivmptf 47314 refdivmptf 47315 fdivpm 47316 refdivpm 47317 |
Copyright terms: Public domain | W3C validator |