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 ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd

Proof

Step Hyp Ref Expression
1 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
2 cmnmnd ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
3 1 2 ax-mp ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
4 xrge0tps ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp
5 eqeq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 0 ↔ 𝑥 = 0 ) )
6 fveq2 ⊢ ( 𝑦 = 𝑥 → ( log ‘ 𝑦 ) = ( log ‘ 𝑥 ) )
7 6 negeqd ⊢ ( 𝑦 = 𝑥 → - ( log ‘ 𝑦 ) = - ( log ‘ 𝑥 ) )
8 5 7 ifbieq2d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) = if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
9 8 cbvmptv ⊢ ( 𝑦 ∈ ( 0 [,] 1 ) ↦ if ( 𝑦 = 0 , +∞ , - ( log ‘ 𝑦 ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 = 0 , +∞ , - ( log ‘ 𝑥 ) ) )
10 eqid ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) )
11 eqid ⊢ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) = ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) )
12 9 10 11 xrge0pluscn ⊢ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ∈ ( ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ×t ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) )
13 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
14 eqid ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
15 xrsadd ⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
16 xaddf ⊢ +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ*
17 ffn ⊢ ( +𝑒 : ( ℝ* × ℝ* ) ⟶ ℝ* → +𝑒 Fn ( ℝ* × ℝ* ) )
18 16 17 ax-mp ⊢ +𝑒 Fn ( ℝ* × ℝ* )
19 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
20 13 14 15 18 19 ressplusf ⊢ ( +𝑓 ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) = ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) )
21 20 eqcomi ⊢ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) = ( +𝑓 ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
22 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
23 ovex ⊢ ( 0 [,] +∞ ) ∈ V
24 xrstset ⊢ ( ordTop ‘ ≤ ) = ( TopSet ‘ ℝ*𝑠 )
25 14 24 resstset ⊢ ( ( 0 [,] +∞ ) ∈ V → ( ordTop ‘ ≤ ) = ( TopSet ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ) )
26 23 25 ax-mp ⊢ ( ordTop ‘ ≤ ) = ( TopSet ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
27 22 26 topnval ⊢ ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
28 21 27 istmd ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd ↔ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ∧ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp ∧ ( +𝑒 ↾ ( ( 0 [,] +∞ ) × ( 0 [,] +∞ ) ) ) ∈ ( ( ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ×t ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) Cn ( ( ordTop ‘ ≤ ) ↾t ( 0 [,] +∞ ) ) ) ) )
29 3 4 12 28 mpbir3an ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopMnd