![]() |
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 6357 | . . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) | |
2 | elssuni 4603 | . . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}) |
4 | uniun 4593 | . . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅}) | |
5 | 0ex 4924 | . . . . 5 ⊢ ∅ ∈ V | |
6 | 5 | unisn 4589 | . . . 4 ⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 3915 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅) |
8 | un0 4111 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹 | |
9 | 4, 7, 8 | 3eqtri 2797 | . 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹 |
10 | 3, 9 | sseqtri 3786 | 1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2145 ∪ cun 3721 ⊆ wss 3723 ∅c0 4063 {csn 4316 ∪ cuni 4574 ran crn 5250 ‘cfv 6031 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3588 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-cnv 5257 df-dm 5259 df-rn 5260 df-iota 5994 df-fv 6039 |
This theorem is referenced by: ovssunirn 6826 marypha2lem1 8497 acnlem 9071 fin23lem29 9365 itunitc 9445 hsmexlem5 9454 wunfv 9756 wunex2 9762 strfvss 16087 prdsval 16323 prdsbas 16325 prdsplusg 16326 prdsmulr 16327 prdsvsca 16328 prdshom 16335 mreunirn 16469 mrcfval 16476 mrcssv 16482 mrisval 16498 sscpwex 16682 wunfunc 16766 catcxpccl 17055 comppfsc 21556 filunirn 21906 elflim 21995 flffval 22013 fclsval 22032 isfcls 22033 fcfval 22057 tsmsxplem1 22176 xmetunirn 22362 mopnval 22463 tmsval 22506 cfilfval 23281 caufval 23292 issgon 30526 elrnsiga 30529 volmeas 30634 omssubadd 30702 neibastop2lem 32692 ismtyval 33931 dicval 36986 ismrc 37790 nacsfix 37801 hbt 38226 |
Copyright terms: Public domain | W3C validator |