Theorem xrgtso

Description: 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	xrgtso	$$⊢{<}^{-1}\mathrm{Or}{ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
2		cnvso	$$⊢<\mathrm{Or}{ℝ}^{*}\leftrightarrow {<}^{-1}\mathrm{Or}{ℝ}^{*}$$
3	1 2	mpbi	$$⊢{<}^{-1}\mathrm{Or}{ℝ}^{*}$$