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 6802 | . . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) | |
2 | elssuni 4871 | . . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}) |
4 | uniun 4864 | . . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅}) | |
5 | 0ex 5231 | . . . . 5 ⊢ ∅ ∈ V | |
6 | 5 | unisn 4861 | . . . 4 ⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 4094 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅) |
8 | un0 4324 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹 | |
9 | 4, 7, 8 | 3eqtri 2770 | . 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹 |
10 | 3, 9 | sseqtri 3957 | 1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ∪ cun 3885 ⊆ wss 3887 ∅c0 4256 {csn 4561 ∪ cuni 4839 ran crn 5590 ‘cfv 6433 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-cnv 5597 df-dm 5599 df-rn 5600 df-iota 6391 df-fv 6441 |
This theorem is referenced by: ovssunirn 7311 marypha2lem1 9194 acnlem 9804 fin23lem29 10097 itunitc 10177 hsmexlem5 10186 wunfv 10488 wunex2 10494 strfvss 16888 prdsvallem 17165 prdsval 17166 prdsbas 17168 prdsplusg 17169 prdsmulr 17170 prdsvsca 17171 prdshom 17178 mreunirn 17310 mrcfval 17317 mrcssv 17323 mrisval 17339 sscpwex 17527 wunfunc 17614 wunfuncOLD 17615 catcxpccl 17924 catcxpcclOLD 17925 comppfsc 22683 filunirn 23033 elflim 23122 flffval 23140 fclsval 23159 isfcls 23160 fcfval 23184 tsmsxplem1 23304 xmetunirn 23490 mopnval 23591 tmsval 23636 cfilfval 24428 caufval 24439 issgon 32091 elrnsiga 32094 volmeas 32199 omssubadd 32267 neibastop2lem 34549 ctbssinf 35577 ismtyval 35958 dicval 39190 ismrc 40523 nacsfix 40534 hbt 40955 |
Copyright terms: Public domain | W3C validator |