Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > xrge0base | Structured version Visualization version GIF version |
Description: The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
Ref | Expression |
---|---|
xrge0base | ⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iccssxr 13151 | . . 3 ⊢ (0[,]+∞) ⊆ ℝ* | |
2 | df-ss 3905 | . . 3 ⊢ ((0[,]+∞) ⊆ ℝ* ↔ ((0[,]+∞) ∩ ℝ*) = (0[,]+∞)) | |
3 | 1, 2 | mpbi 229 | . 2 ⊢ ((0[,]+∞) ∩ ℝ*) = (0[,]+∞) |
4 | ovex 7302 | . . 3 ⊢ (0[,]+∞) ∈ V | |
5 | eqid 2738 | . . . 4 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) = (ℝ*𝑠 ↾s (0[,]+∞)) | |
6 | xrsbas 20603 | . . . 4 ⊢ ℝ* = (Base‘ℝ*𝑠) | |
7 | 5, 6 | ressbas 16936 | . . 3 ⊢ ((0[,]+∞) ∈ V → ((0[,]+∞) ∩ ℝ*) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞)))) |
8 | 4, 7 | ax-mp 5 | . 2 ⊢ ((0[,]+∞) ∩ ℝ*) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) |
9 | 3, 8 | eqtr3i 2768 | 1 ⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∈ wcel 2106 Vcvv 3431 ∩ cin 3887 ⊆ wss 3888 ‘cfv 6428 (class class class)co 7269 0cc0 10860 +∞cpnf 10995 ℝ*cxr 10997 [,]cicc 13071 Basecbs 16901 ↾s cress 16930 ℝ*𝑠cxrs 17200 |
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-pow 5288 ax-pr 5352 ax-un 7580 ax-cnex 10916 ax-resscn 10917 ax-1cn 10918 ax-icn 10919 ax-addcl 10920 ax-addrcl 10921 ax-mulcl 10922 ax-mulrcl 10923 ax-mulcom 10924 ax-addass 10925 ax-mulass 10926 ax-distr 10927 ax-i2m1 10928 ax-1ne0 10929 ax-1rid 10930 ax-rnegex 10931 ax-rrecex 10932 ax-cnre 10933 ax-pre-lttri 10934 ax-pre-lttrn 10935 ax-pre-ltadd 10936 ax-pre-mulgt0 10937 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 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-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3433 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4259 df-if 4462 df-pw 4537 df-sn 4564 df-pr 4566 df-tp 4568 df-op 4570 df-uni 4842 df-iun 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5486 df-eprel 5492 df-po 5500 df-so 5501 df-fr 5541 df-we 5543 df-xp 5592 df-rel 5593 df-cnv 5594 df-co 5595 df-dm 5596 df-rn 5597 df-res 5598 df-ima 5599 df-pred 6197 df-ord 6264 df-on 6265 df-lim 6266 df-suc 6267 df-iota 6386 df-fun 6430 df-fn 6431 df-f 6432 df-f1 6433 df-fo 6434 df-f1o 6435 df-fv 6436 df-riota 7226 df-ov 7272 df-oprab 7273 df-mpo 7274 df-om 7705 df-1st 7822 df-2nd 7823 df-frecs 8086 df-wrecs 8117 df-recs 8191 df-rdg 8230 df-1o 8286 df-er 8487 df-en 8723 df-dom 8724 df-sdom 8725 df-fin 8726 df-pnf 11000 df-mnf 11001 df-xr 11002 df-ltxr 11003 df-le 11004 df-sub 11196 df-neg 11197 df-nn 11963 df-2 12025 df-3 12026 df-4 12027 df-5 12028 df-6 12029 df-7 12030 df-8 12031 df-9 12032 df-n0 12223 df-z 12309 df-dec 12427 df-uz 12572 df-icc 13075 df-fz 13229 df-struct 16837 df-sets 16854 df-slot 16872 df-ndx 16884 df-base 16902 df-ress 16931 df-plusg 16964 df-mulr 16965 df-tset 16970 df-ple 16971 df-ds 16973 df-xrs 17202 |
This theorem is referenced by: xrge0omnd 31324 xrge0slmod 31535 xrge0iifmhm 31876 xrge0tmdALT 31883 esumcl 31985 esumgsum 32000 esumf1o 32005 esumsplit 32008 esumadd 32012 gsumesum 32014 esumlub 32015 esumaddf 32016 esumcst 32018 esumsnf 32019 esumss 32027 esumpfinvallem 32029 esumpfinval 32030 esumpfinvalf 32031 esumcocn 32035 esum2d 32048 sitmcl 32305 |
Copyright terms: Public domain | W3C validator |