![]() |
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 8098 | . . 3 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}}) | |
2 | ssrab2 4041 | . . 3 ⊢ {𝑖 ∈ dom 𝐹 ∣ (𝐹 “ {𝑖}) ≠ {𝑍}} ⊆ dom 𝐹 | |
3 | 1, 2 | eqsstrdi 4002 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) ⊆ dom 𝐹) |
4 | supp0prc 8099 | . . 3 ⊢ (¬ (𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) | |
5 | 0ss 4360 | . . 3 ⊢ ∅ ⊆ dom 𝐹 | |
6 | 4, 5 | eqsstrdi 4002 | . 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 397 ∈ wcel 2107 ≠ wne 2940 {crab 3406 Vcvv 3447 ⊆ wss 3914 ∅c0 4286 {csn 4590 dom cdm 5637 “ cima 5640 (class class class)co 7361 supp csupp 8096 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 ax-un 7676 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-sbc 3744 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-opab 5172 df-id 5535 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-rn 5648 df-res 5649 df-ima 5650 df-iota 6452 df-fun 6502 df-fv 6508 df-ov 7364 df-oprab 7365 df-mpo 7366 df-supp 8097 |
This theorem is referenced by: snopsuppss 8114 wemapso2lem 9496 cantnfcl 9611 cantnfle 9615 cantnflt 9616 cantnff 9618 cantnfres 9621 cantnfp1lem3 9624 cantnflem1b 9630 cantnflem1 9633 cantnflem3 9635 cnfcomlem 9643 cnfcom 9644 cnfcom3lem 9647 cnfcom3 9648 fsuppmapnn0fiublem 13904 fsuppmapnn0fiub 13905 gsumval3lem1 19690 gsumval3lem2 19691 gsumval3 19692 gsumzres 19694 gsumzcl2 19695 gsumzf1o 19697 gsumzaddlem 19706 gsumconst 19719 gsumzoppg 19729 gsum2d 19757 dpjidcl 19845 gsumfsum 20887 regsumsupp 21049 frlmlbs 21226 psrass1lemOLD 21365 psrass1lem 21368 psrass1 21397 psrass23l 21400 psrcom 21401 psrass23 21402 mplcoe1 21461 psropprmul 21632 coe1mul2 21663 tsmsgsum 23513 rrxcph 24779 rrxsuppss 24790 rrxmval 24792 mdegfval 25450 mdegleb 25452 mdegldg 25454 deg1mul3le 25504 wilthlem3 26442 suppovss 31651 fressupp 31656 ressupprn 31658 supppreima 31659 fsupprnfi 31660 fsuppcurry1 31696 fsuppcurry2 31697 gsumhashmul 31954 elrspunidl 32258 fedgmullem1 32388 zarcmplem 32526 fdivmpt 46716 fdivmptf 46717 refdivmptf 46718 fdivpm 46719 refdivpm 46720 |
Copyright terms: Public domain | W3C validator |