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