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 6696 | . . 3 ⊢ (𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) | |
2 | elssuni 4825 | . . 3 ⊢ ((𝐹‘𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅})) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ (𝐹‘𝑋) ⊆ ∪ (ran 𝐹 ∪ {∅}) |
4 | uniun 4818 | . . 3 ⊢ ∪ (ran 𝐹 ∪ {∅}) = (∪ ran 𝐹 ∪ ∪ {∅}) | |
5 | 0ex 5172 | . . . . 5 ⊢ ∅ ∈ V | |
6 | 5 | unisn 4815 | . . . 4 ⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 4048 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∪ {∅}) = (∪ ran 𝐹 ∪ ∅) |
8 | un0 4276 | . . 3 ⊢ (∪ ran 𝐹 ∪ ∅) = ∪ ran 𝐹 | |
9 | 4, 7, 8 | 3eqtri 2765 | . 2 ⊢ ∪ (ran 𝐹 ∪ {∅}) = ∪ ran 𝐹 |
10 | 3, 9 | sseqtri 3911 | 1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 ∪ cun 3839 ⊆ wss 3841 ∅c0 4209 {csn 4513 ∪ cuni 4793 ran crn 5520 ‘cfv 6333 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-ne 2935 df-ral 3058 df-rex 3059 df-v 3399 df-sbc 3680 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-cnv 5527 df-dm 5529 df-rn 5530 df-iota 6291 df-fv 6341 |
This theorem is referenced by: ovssunirn 7200 marypha2lem1 8965 acnlem 9541 fin23lem29 9834 itunitc 9914 hsmexlem5 9923 wunfv 10225 wunex2 10231 strfvss 16602 prdsval 16824 prdsbas 16826 prdsplusg 16827 prdsmulr 16828 prdsvsca 16829 prdshom 16836 mreunirn 16968 mrcfval 16975 mrcssv 16981 mrisval 16997 sscpwex 17183 wunfunc 17267 catcxpccl 17566 comppfsc 22276 filunirn 22626 elflim 22715 flffval 22733 fclsval 22752 isfcls 22753 fcfval 22777 tsmsxplem1 22897 xmetunirn 23083 mopnval 23184 tmsval 23227 cfilfval 24009 caufval 24020 issgon 31653 elrnsiga 31656 volmeas 31761 omssubadd 31829 neibastop2lem 34179 ctbssinf 35189 ismtyval 35570 dicval 38802 ismrc 40079 nacsfix 40090 hbt 40511 |
Copyright terms: Public domain | W3C validator |