Metamath Proof Explorer

Theorem xrge00

Description: The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Assertion xrge00 ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞

Proof

Step Hyp Ref Expression
1 eqid ⊢ ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
2 1 xrs1mnd ⊢ ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ∈ Mnd
3 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
4 cmnmnd ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd
5 3 4 ax-mp ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd
6 mnflt0 ⊢ −∞ < 0
7 mnfxr ⊢ −∞ ∈ ℝ *
8 0xr ⊢ 0 ∈ ℝ *
9 xrltnle ⊢ −∞ ∈ ℝ * ∧ 0 ∈ ℝ * → −∞ < 0 ↔ ¬ 0 ≤ −∞
10 7 8 9 mp2an ⊢ −∞ < 0 ↔ ¬ 0 ≤ −∞
11 6 10 mpbi ⊢ ¬ 0 ≤ −∞
12 11 intnan ⊢ ¬ −∞ ∈ ℝ * ∧ 0 ≤ −∞
13 elxrge0 ⊢ −∞ ∈ 0 +∞ ↔ −∞ ∈ ℝ * ∧ 0 ≤ −∞
14 12 13 mtbir ⊢ ¬ −∞ ∈ 0 +∞
15 difsn ⊢ ¬ −∞ ∈ 0 +∞ → 0 +∞ ∖ −∞ = 0 +∞
16 14 15 ax-mp ⊢ 0 +∞ ∖ −∞ = 0 +∞
17 iccssxr ⊢ 0 +∞ ⊆ ℝ *
18 ssdif ⊢ 0 +∞ ⊆ ℝ * → 0 +∞ ∖ −∞ ⊆ ℝ * ∖ −∞
19 17 18 ax-mp ⊢ 0 +∞ ∖ −∞ ⊆ ℝ * ∖ −∞
20 16 19 eqsstrri ⊢ 0 +∞ ⊆ ℝ * ∖ −∞
21 0e0iccpnf ⊢ 0 ∈ 0 +∞
22 difss ⊢ ℝ * ∖ −∞ ⊆ ℝ *
23 df-ss ⊢ ℝ * ∖ −∞ ⊆ ℝ * ↔ ℝ * ∖ −∞ ∩ ℝ * = ℝ * ∖ −∞
24 22 23 mpbi ⊢ ℝ * ∖ −∞ ∩ ℝ * = ℝ * ∖ −∞
25 xrex ⊢ ℝ * ∈ V
26 difexg ⊢ ℝ * ∈ V → ℝ * ∖ −∞ ∈ V
27 25 26 ax-mp ⊢ ℝ * ∖ −∞ ∈ V
28 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
29 1 28 ressbas ⊢ ℝ * ∖ −∞ ∈ V → ℝ * ∖ −∞ ∩ ℝ * = Base ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
30 27 29 ax-mp ⊢ ℝ * ∖ −∞ ∩ ℝ * = Base ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
31 24 30 eqtr3i ⊢ ℝ * ∖ −∞ = Base ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
32 1 xrs10 ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞
33 ovex ⊢ 0 +∞ ∈ V
34 ressress ⊢ ℝ * ∖ −∞ ∈ V ∧ 0 +∞ ∈ V → ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ∩ 0 +∞
35 27 33 34 mp2an ⊢ ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ∩ 0 +∞
36 dfss ⊢ 0 +∞ ⊆ ℝ * ∖ −∞ ↔ 0 +∞ = 0 +∞ ∩ ℝ * ∖ −∞
37 20 36 mpbi ⊢ 0 +∞ = 0 +∞ ∩ ℝ * ∖ −∞
38 incom ⊢ 0 +∞ ∩ ℝ * ∖ −∞ = ℝ * ∖ −∞ ∩ 0 +∞
39 37 38 eqtr2i ⊢ ℝ * ∖ −∞ ∩ 0 +∞ = 0 +∞
40 39 oveq2i ⊢ ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ∩ 0 +∞ = ℝ 𝑠 * ↾ 𝑠 0 +∞
41 35 40 eqtr2i ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ↾ 𝑠 0 +∞
42 31 32 41 submnd0 ⊢ ℝ 𝑠 * ↾ 𝑠 ℝ * ∖ −∞ ∈ Mnd ∧ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd ∧ 0 +∞ ⊆ ℝ * ∖ −∞ ∧ 0 ∈ 0 +∞ → 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞
43 2 5 20 21 42 mp4an ⊢ 0 = 0 ℝ 𝑠 * ↾ 𝑠 0 +∞