Theorem xrslt

Description: The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Assertion	xrslt	$$⊢<={<}_{{ℝ}_{𝑠}^{*}}$$

Proof

Step	Hyp	Ref	Expression
1		dflt2	$$⊢<=\le \setminus \mathrm{I}$$
2		xrsex	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{V}$$
3		xrsle	$$⊢\le ={\le }_{{ℝ}_{𝑠}^{*}}$$
4		eqid	$$⊢{<}_{{ℝ}_{𝑠}^{*}}={<}_{{ℝ}_{𝑠}^{*}}$$
5	3 4	pltfval	$$⊢{ℝ}_{𝑠}^{*}\in \mathrm{V}\to {<}_{{ℝ}_{𝑠}^{*}}=\le \setminus \mathrm{I}$$
6	2 5	ax-mp	$$⊢{<}_{{ℝ}_{𝑠}^{*}}=\le \setminus \mathrm{I}$$
7	1 6	eqtr4i	$$⊢<={<}_{{ℝ}_{𝑠}^{*}}$$