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 → if y = 0 +∞ − log ⁡ y = if x = 0 +∞ − log ⁡ x
9 8 cbvmptv ⊢ y ∈ 0 1 ⟼ if y = 0 +∞ − log ⁡ y = x ∈ 0 1 ⟼ if x = 0 +∞ − log ⁡ x
10 eqid ⊢ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
11 eqid ⊢ + 𝑒 ↾ 0 +∞ × 0 +∞ = + 𝑒 ↾ 0 +∞ × 0 +∞
12 9 10 11 xrge0pluscn ⊢ + 𝑒 ↾ 0 +∞ × 0 +∞ ∈ ordTop ⁡ ≤ ↾ 𝑡 0 +∞ × t ordTop ⁡ ≤ ↾ 𝑡 0 +∞ Cn ordTop ⁡ ≤ ↾ 𝑡 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 +∞ × t ordTop ⁡ ≤ ↾ 𝑡 0 +∞ Cn ordTop ⁡ ≤ ↾ 𝑡 0 +∞
29 3 4 12 28 mpbir3an ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopMnd