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+∞