Theorem xrsp0

Description: The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018) (Proof shortened by AV, 28-Sep-2020)

	Ref	Expression
Assertion	xrsp0	$$⊢\mathrm{-\infty }=\mathrm{0.}\left({ℝ}_{𝑠}^{*}\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrsex	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{V}$$
2		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
3		eqid	$$⊢\mathrm{glb}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{glb}\left({ℝ}_{𝑠}^{*}\right)$$
4		eqid	$$⊢\mathrm{0.}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{0.}\left({ℝ}_{𝑠}^{*}\right)$$
5	2 3 4	p0val	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{V}\to \mathrm{0.}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{glb}\left({ℝ}_{𝑠}^{*}\right)\left({ℝ}^{*}\right)$$
6	1 5	ax-mp	$$⊢\mathrm{0.}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{glb}\left({ℝ}_{𝑠}^{*}\right)\left({ℝ}^{*}\right)$$
7		ssid	$$⊢{ℝ}^{*}\subseteq {ℝ}^{*}$$
8		xrslt	$$⊢<={<}_{{ℝ}_{𝑠}^{*}}$$
9		xrstos	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{Toset}$$
10	9	a1i	$$⊢{ℝ}^{*}\subseteq {ℝ}^{*}\to {ℝ}_{𝑠}^{*}\in \mathrm{Toset}$$
11		id	$$⊢{ℝ}^{*}\subseteq {ℝ}^{*}\to {ℝ}^{*}\subseteq {ℝ}^{*}$$
12	2 8 10 11	tosglb	$$⊢{ℝ}^{*}\subseteq {ℝ}^{*}\to \mathrm{glb}\left({ℝ}_{𝑠}^{*}\right)\left({ℝ}^{*}\right)=inf\left({ℝ}^{*},{ℝ}^{*},<\right)$$
13	7 12	ax-mp	$$⊢\mathrm{glb}\left({ℝ}_{𝑠}^{*}\right)\left({ℝ}^{*}\right)=inf\left({ℝ}^{*},{ℝ}^{*},<\right)$$
14		xrinfm	$$⊢inf\left({ℝ}^{*},{ℝ}^{*},<\right)=\mathrm{-\infty }$$
15	6 13 14	3eqtrri	$$⊢\mathrm{-\infty }=\mathrm{0.}\left({ℝ}_{𝑠}^{*}\right)$$