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