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 ⊢ℝ𝑠*↾𝑠0+∞∈TopMnd

Proof

Step Hyp Ref Expression
1 xrge0cmn ⊢ℝ𝑠*↾𝑠0+∞∈CMnd
2 cmnmnd ⊢ℝ𝑠*↾𝑠0+∞∈CMnd→ℝ𝑠*↾𝑠0+∞∈Mnd
3 1 2 ax-mp ⊢ℝ𝑠*↾𝑠0+∞∈Mnd
4 xrge0tps ⊢ℝ𝑠*↾𝑠0+∞∈TopSp
5 eqeq1 ⊢y=x→y=0↔x=0
6 fveq2 ⊢y=x→log⁡y=log⁡x
7 6 negeqd ⊢y=x→−log⁡y=−log⁡x
8 5 7 ifbieq2d ⊢y=x→ify=0+∞−log⁡y=ifx=0+∞−log⁡x
9 8 cbvmptv ⊢y∈01⟼ify=0+∞−log⁡y=x∈01⟼ifx=0+∞−log⁡x
10 eqid ⊢ordTop⁡≤↾𝑡0+∞=ordTop⁡≤↾𝑡0+∞
11 eqid ⊢+𝑒↾0+∞×0+∞=+𝑒↾0+∞×0+∞
12 9 10 11 xrge0pluscn ⊢+𝑒↾0+∞×0+∞∈ordTop⁡≤↾𝑡0+∞×tordTop⁡≤↾𝑡0+∞CnordTop⁡≤↾𝑡0+∞
13 xrsbas ⊢ℝ*=Baseℝ𝑠*
14 eqid ⊢ℝ𝑠*↾𝑠0+∞=ℝ𝑠*↾𝑠0+∞
15 xrsadd ⊢+𝑒=+ℝ𝑠*
16 xaddf ⊢+𝑒:ℝ*×ℝ*⟶ℝ*
17 ffn ⊢+𝑒:ℝ*×ℝ*⟶ℝ*→+𝑒Fnℝ*×ℝ*
18 16 17 ax-mp ⊢+𝑒Fnℝ*×ℝ*
19 iccssxr ⊢0+∞⊆ℝ*
20 13 14 15 18 19 ressplusf ⊢+𝑓⁡ℝ𝑠*↾𝑠0+∞=+𝑒↾0+∞×0+∞
21 20 eqcomi ⊢+𝑒↾0+∞×0+∞=+𝑓⁡ℝ𝑠*↾𝑠0+∞
22 xrge0base ⊢0+∞=Baseℝ𝑠*↾𝑠0+∞
23 ovex ⊢0+∞∈V
24 xrstset ⊢ordTop⁡≤=TopSet⁡ℝ𝑠*
25 14 24 resstset ⊢0+∞∈V→ordTop⁡≤=TopSet⁡ℝ𝑠*↾𝑠0+∞
26 23 25 ax-mp ⊢ordTop⁡≤=TopSet⁡ℝ𝑠*↾𝑠0+∞
27 22 26 topnval ⊢ordTop⁡≤↾𝑡0+∞=TopOpen⁡ℝ𝑠*↾𝑠0+∞
28 21 27 istmd ⊢ℝ𝑠*↾𝑠0+∞∈TopMnd↔ℝ𝑠*↾𝑠0+∞∈Mnd∧ℝ𝑠*↾𝑠0+∞∈TopSp∧+𝑒↾0+∞×0+∞∈ordTop⁡≤↾𝑡0+∞×tordTop⁡≤↾𝑡0+∞CnordTop⁡≤↾𝑡0+∞
29 3 4 12 28 mpbir3an ⊢ℝ𝑠*↾𝑠0+∞∈TopMnd