Metamath Proof Explorer

Theorem xrge0tmdALT

Description: Alternate proof of xrge0tmd . (Contributed by Thierry Arnoux, 26-Mar-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion xrge0tmdALT 
|- ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd

Proof

Step Hyp Ref Expression
1 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
2 cmnmnd 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
3 1 2 ax-mp 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
4 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
5 eqeq1 
 |-  ( y = x -> ( y = 0 <-> x = 0 ) )
6 fveq2 
 |-  ( y = x -> ( log ` y ) = ( log ` x ) )
7 6 negeqd 
 |-  ( y = x -> -u ( log ` y ) = -u ( log ` x ) )
8 5 7 ifbieq2d 
 |-  ( y = x -> if ( y = 0 , +oo , -u ( log ` y ) ) = if ( x = 0 , +oo , -u ( log ` x ) ) )
9 8 cbvmptv 
 |-  ( y e. ( 0 [,] 1 ) |-> if ( y = 0 , +oo , -u ( log ` y ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x = 0 , +oo , -u ( log ` x ) ) )
10 eqid 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
11 eqid 
 |-  ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) = ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) )
12 9 10 11 xrge0pluscn 
 |-  ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) e. ( ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) tX ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) Cn ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) )
13 xrsbas 
 |-  RR* = ( Base ` RR*s )
14 eqid 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
15 xrsadd 
 |-  +e = ( +g ` RR*s )
16 xaddf 
 |-  +e : ( RR* X. RR* ) --> RR*
17 ffn 
 |-  ( +e : ( RR* X. RR* ) --> RR* -> +e Fn ( RR* X. RR* ) )
18 16 17 ax-mp 
 |-  +e Fn ( RR* X. RR* )
19 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
20 13 14 15 18 19 ressplusf 
 |-  ( +f ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) )
21 20 eqcomi 
 |-  ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) = ( +f ` ( RR*s |`s ( 0 [,] +oo ) ) )
22 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
23 ovex 
 |-  ( 0 [,] +oo ) e. _V
24 xrstset 
 |-  ( ordTop ` <_ ) = ( TopSet ` RR*s )
25 14 24 resstset 
 |-  ( ( 0 [,] +oo ) e. _V -> ( ordTop ` <_ ) = ( TopSet ` ( RR*s |`s ( 0 [,] +oo ) ) ) )
26 23 25 ax-mp 
 |-  ( ordTop ` <_ ) = ( TopSet ` ( RR*s |`s ( 0 [,] +oo ) ) )
27 22 26 topnval 
 |-  ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
28 21 27 istmd 
 |-  ( ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd <-> ( ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd /\ ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp /\ ( +e |` ( ( 0 [,] +oo ) X. ( 0 [,] +oo ) ) ) e. ( ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) tX ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) Cn ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) ) )
29 3 4 12 28 mpbir3an 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopMnd