Metamath Proof Explorer

Theorem xrsex

Description: The extended real structure is a set. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xrsex 
|- RR*s e. _V

Proof

Step Hyp Ref Expression
1 df-xrs 
 |-  RR*s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )
2 tpex 
 |-  { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } e. _V
3 tpex 
 |-  { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } e. _V
4 2 3 unex 
 |-  ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } ) e. _V
5 1 4 eqeltri 
 |-  RR*s e. _V