![]() |
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 6673 | . . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) | |
2 | elssuni 4830 | . . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}) |
4 | uniun 4823 | . . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅}) | |
5 | 0ex 5175 | . . . . 5 ⊢ ∅ ∈ V | |
6 | 5 | unisn 4820 | . . . 4 ⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 4087 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅) |
8 | un0 4298 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹 | |
9 | 4, 7, 8 | 3eqtri 2825 | . 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹 |
10 | 3, 9 | sseqtri 3951 | 1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 ∪ cun 3879 ⊆ wss 3881 ∅c0 4243 {csn 4525 ∪ cuni 4800 ran crn 5520 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-cnv 5527 df-dm 5529 df-rn 5530 df-iota 6283 df-fv 6332 |
This theorem is referenced by: ovssunirn 7171 marypha2lem1 8883 acnlem 9459 fin23lem29 9752 itunitc 9832 hsmexlem5 9841 wunfv 10143 wunex2 10149 strfvss 16498 prdsval 16720 prdsbas 16722 prdsplusg 16723 prdsmulr 16724 prdsvsca 16725 prdshom 16732 mreunirn 16864 mrcfval 16871 mrcssv 16877 mrisval 16893 sscpwex 17077 wunfunc 17161 catcxpccl 17449 comppfsc 22137 filunirn 22487 elflim 22576 flffval 22594 fclsval 22613 isfcls 22614 fcfval 22638 tsmsxplem1 22758 xmetunirn 22944 mopnval 23045 tmsval 23088 cfilfval 23868 caufval 23879 issgon 31492 elrnsiga 31495 volmeas 31600 omssubadd 31668 neibastop2lem 33821 ctbssinf 34823 ismtyval 35238 dicval 38472 ismrc 39642 nacsfix 39653 hbt 40074 |
Copyright terms: Public domain | W3C validator |