![]() |
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 6476 | . . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) | |
2 | elssuni 4704 | . . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}) |
4 | uniun 4694 | . . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅}) | |
5 | 0ex 5028 | . . . . 5 ⊢ ∅ ∈ V | |
6 | 5 | unisn 4689 | . . . 4 ⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 3987 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅) |
8 | un0 4193 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹 | |
9 | 4, 7, 8 | 3eqtri 2806 | . 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹 |
10 | 3, 9 | sseqtri 3856 | 1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ∪ cun 3790 ⊆ wss 3792 ∅c0 4141 {csn 4398 ∪ cuni 4673 ran crn 5358 ‘cfv 6137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-cnv 5365 df-dm 5367 df-rn 5368 df-iota 6101 df-fv 6145 |
This theorem is referenced by: ovssunirn 6959 marypha2lem1 8631 acnlem 9206 fin23lem29 9500 itunitc 9580 hsmexlem5 9589 wunfv 9891 wunex2 9897 strfvss 16289 prdsval 16512 prdsbas 16514 prdsplusg 16515 prdsmulr 16516 prdsvsca 16517 prdshom 16524 mreunirn 16658 mrcfval 16665 mrcssv 16671 mrisval 16687 sscpwex 16871 wunfunc 16955 catcxpccl 17244 comppfsc 21755 filunirn 22105 elflim 22194 flffval 22212 fclsval 22231 isfcls 22232 fcfval 22256 tsmsxplem1 22375 xmetunirn 22561 mopnval 22662 tmsval 22705 cfilfval 23481 caufval 23492 issgon 30792 elrnsiga 30795 volmeas 30900 omssubadd 30968 neibastop2lem 32951 ismtyval 34232 dicval 37339 ismrc 38238 nacsfix 38249 hbt 38673 |
Copyright terms: Public domain | W3C validator |