Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fvssunirn | Structured version Visualization version GIF version |
Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
fvssunirn | ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvrn0 6692 | . . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) | |
2 | elssuni 4861 | . . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}) |
4 | uniun 4851 | . . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅}) | |
5 | 0ex 5203 | . . . . 5 ⊢ ∅ ∈ V | |
6 | 5 | unisn 4848 | . . . 4 ⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 4135 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅) |
8 | un0 4343 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹 | |
9 | 4, 7, 8 | 3eqtri 2848 | . 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹 |
10 | 3, 9 | sseqtri 4002 | 1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ∪ cun 3933 ⊆ wss 3935 ∅c0 4290 {csn 4559 ∪ cuni 4832 ran crn 5550 ‘cfv 6349 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-cnv 5557 df-dm 5559 df-rn 5560 df-iota 6308 df-fv 6357 |
This theorem is referenced by: ovssunirn 7181 marypha2lem1 8888 acnlem 9463 fin23lem29 9752 itunitc 9832 hsmexlem5 9841 wunfv 10143 wunex2 10149 strfvss 16496 prdsval 16718 prdsbas 16720 prdsplusg 16721 prdsmulr 16722 prdsvsca 16723 prdshom 16730 mreunirn 16862 mrcfval 16869 mrcssv 16875 mrisval 16891 sscpwex 17075 wunfunc 17159 catcxpccl 17447 comppfsc 22070 filunirn 22420 elflim 22509 flffval 22527 fclsval 22546 isfcls 22547 fcfval 22571 tsmsxplem1 22690 xmetunirn 22876 mopnval 22977 tmsval 23020 cfilfval 23796 caufval 23807 issgon 31282 elrnsiga 31285 volmeas 31390 omssubadd 31458 neibastop2lem 33606 ctbssinf 34570 ismtyval 34961 dicval 38194 ismrc 39178 nacsfix 39189 hbt 39610 |
Copyright terms: Public domain | W3C validator |