Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xrsbas | Structured version Visualization version GIF version |
Description: The base set of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Ref | Expression |
---|---|
xrsbas | ⊢ ℝ* = (Base‘ℝ*𝑠) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrex 12608 | . 2 ⊢ ℝ* ∈ V | |
2 | df-xrs 17035 | . . 3 ⊢ ℝ*𝑠 = ({〈(Base‘ndx), ℝ*〉, 〈(+g‘ndx), +𝑒 〉, 〈(.r‘ndx), ·e 〉} ∪ {〈(TopSet‘ndx), (ordTop‘ ≤ )〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 ≤ 𝑦, (𝑦 +𝑒 -𝑒𝑥), (𝑥 +𝑒 -𝑒𝑦)))〉}) | |
3 | 2 | odrngbas 16939 | . 2 ⊢ (ℝ* ∈ V → ℝ* = (Base‘ℝ*𝑠)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ ℝ* = (Base‘ℝ*𝑠) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∈ wcel 2111 Vcvv 3421 ifcif 4454 class class class wbr 5068 ‘cfv 6398 (class class class)co 7232 ∈ cmpo 7234 ℝ*cxr 10891 ≤ cle 10893 -𝑒cxne 12726 +𝑒 cxad 12727 ·e cxmu 12728 Basecbs 16788 ordTopcordt 17032 ℝ*𝑠cxrs 17033 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-sep 5207 ax-nul 5214 ax-pow 5273 ax-pr 5337 ax-un 7542 ax-cnex 10810 ax-resscn 10811 ax-1cn 10812 ax-icn 10813 ax-addcl 10814 ax-addrcl 10815 ax-mulcl 10816 ax-mulrcl 10817 ax-mulcom 10818 ax-addass 10819 ax-mulass 10820 ax-distr 10821 ax-i2m1 10822 ax-1ne0 10823 ax-1rid 10824 ax-rnegex 10825 ax-rrecex 10826 ax-cnre 10827 ax-pre-lttri 10828 ax-pre-lttrn 10829 ax-pre-ltadd 10830 ax-pre-mulgt0 10831 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3067 df-rex 3068 df-reu 3069 df-rab 3071 df-v 3423 df-sbc 3710 df-csb 3827 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4253 df-if 4455 df-pw 4530 df-sn 4557 df-pr 4559 df-tp 4561 df-op 4563 df-uni 4835 df-iun 4921 df-br 5069 df-opab 5131 df-mpt 5151 df-tr 5177 df-id 5470 df-eprel 5475 df-po 5483 df-so 5484 df-fr 5524 df-we 5526 df-xp 5572 df-rel 5573 df-cnv 5574 df-co 5575 df-dm 5576 df-rn 5577 df-res 5578 df-ima 5579 df-pred 6176 df-ord 6234 df-on 6235 df-lim 6236 df-suc 6237 df-iota 6356 df-fun 6400 df-fn 6401 df-f 6402 df-f1 6403 df-fo 6404 df-f1o 6405 df-fv 6406 df-riota 7189 df-ov 7235 df-oprab 7236 df-mpo 7237 df-om 7664 df-1st 7780 df-2nd 7781 df-wrecs 8068 df-recs 8129 df-rdg 8167 df-1o 8223 df-er 8412 df-en 8648 df-dom 8649 df-sdom 8650 df-fin 8651 df-pnf 10894 df-mnf 10895 df-xr 10896 df-ltxr 10897 df-le 10898 df-sub 11089 df-neg 11090 df-nn 11856 df-2 11918 df-3 11919 df-4 11920 df-5 11921 df-6 11922 df-7 11923 df-8 11924 df-9 11925 df-n0 12116 df-z 12202 df-dec 12319 df-uz 12464 df-fz 13121 df-struct 16728 df-slot 16763 df-ndx 16773 df-base 16789 df-plusg 16843 df-mulr 16844 df-tset 16849 df-ple 16850 df-ds 16852 df-xrs 17035 |
This theorem is referenced by: xrsmcmn 20414 xrsmgm 20426 xrsnsgrp 20427 xrs1mnd 20429 xrs10 20430 xrs1cmn 20431 xrge0subm 20432 xrge0cmn 20433 xrstopn 22132 xrstps 22133 imasdsf1olem 23298 xrge0gsumle 23757 xrge0tsms 23758 xrs0 31030 xrsinvgval 31032 xrsmulgzz 31033 xrstos 31034 xrsclat 31035 xrsp0 31036 xrsp1 31037 xrge0base 31040 xrge00 31041 xrge0mulgnn0 31044 xrge0tsmsd 31063 pnfinf 31183 xrnarchi 31184 xrge0tmdALT 31637 esumpfinvallem 31781 gsumge0cl 43615 sge0tsms 43624 |
Copyright terms: Public domain | W3C validator |