Metamath Proof Explorer

Theorem xrge0base

Description: The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Assertion xrge0base 
|- ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )

Proof

Step Hyp Ref Expression
1 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
2 dfss2 
 |-  ( ( 0 [,] +oo ) C_ RR* <-> ( ( 0 [,] +oo ) i^i RR* ) = ( 0 [,] +oo ) )
3 1 2 mpbi 
 |-  ( ( 0 [,] +oo ) i^i RR* ) = ( 0 [,] +oo )
4 ovex 
 |-  ( 0 [,] +oo ) e. _V
5 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
6 xrsbas 
 |-  RR* = ( Base ` RR*s )
7 5 6 ressbas 
 |-  ( ( 0 [,] +oo ) e. _V -> ( ( 0 [,] +oo ) i^i RR* ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
8 4 7 ax-mp 
 |-  ( ( 0 [,] +oo ) i^i RR* ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
9 3 8 eqtr3i 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )