Theorem xrsp1

Description: The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018)

	Ref	Expression
Assertion	xrsp1	$$⊢\mathrm{+\infty }=\mathrm{1.}\left({ℝ}_{𝑠}^{*}\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrsex	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{V}$$
2		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
3		eqid	$$⊢\mathrm{lub}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{lub}\left({ℝ}_{𝑠}^{*}\right)$$
4		eqid	$$⊢\mathrm{1.}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{1.}\left({ℝ}_{𝑠}^{*}\right)$$
5	2 3 4	p1val	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{V}\to \mathrm{1.}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{lub}\left({ℝ}_{𝑠}^{*}\right)\left({ℝ}^{*}\right)$$
6	1 5	ax-mp	$$⊢\mathrm{1.}\left({ℝ}_{𝑠}^{*}\right)=\mathrm{lub}\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	toslub	$$⊢{ℝ}^{*}\subseteq {ℝ}^{*}\to \mathrm{lub}\left({ℝ}_{𝑠}^{*}\right)\left({ℝ}^{*}\right)=sup\left({ℝ}^{*},{ℝ}^{*},<\right)$$
13	7 12	ax-mp	$$⊢\mathrm{lub}\left({ℝ}_{𝑠}^{*}\right)\left({ℝ}^{*}\right)=sup\left({ℝ}^{*},{ℝ}^{*},<\right)$$
14		xrsup	$$⊢sup\left({ℝ}^{*},{ℝ}^{*},<\right)=\mathrm{+\infty }$$
15	6 13 14	3eqtrri	$$⊢\mathrm{+\infty }=\mathrm{1.}\left({ℝ}_{𝑠}^{*}\right)$$