Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xrsex | Structured version Visualization version Unicode version |
Description: The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Ref | Expression |
---|---|
xrsex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xrs 16162 | . 2 TopSet ordTop | |
2 | tpex 6957 | . . 3 | |
3 | tpex 6957 | . . 3 TopSet ordTop | |
4 | 2, 3 | unex 6956 | . 2 TopSet ordTop |
5 | 1, 4 | eqeltri 2697 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 cvv 3200 cun 3572 cif 4086 ctp 4181 cop 4183 class class class wbr 4653 cfv 5888 (class class class)co 6650 cmpt2 6652 cxr 10073 cle 10075 cxne 11943 cxad 11944 cxmu 11945 cnx 15854 cbs 15857 cplusg 15941 cmulr 15942 TopSetcts 15947 cple 15948 cds 15950 ordTopcordt 16159 cxrs 16160 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-v 3202 df-dif 3577 df-un 3579 df-nul 3916 df-sn 4178 df-pr 4180 df-tp 4182 df-uni 4437 df-xrs 16162 |
This theorem is referenced by: imasdsf1olem 22178 xrslt 29676 xrsmulgzz 29678 xrstos 29679 xrsp0 29681 xrsp1 29682 pnfinf 29737 xrnarchi 29738 |
Copyright terms: Public domain | W3C validator |