Theorem lern

Description: The range of <_ is RR* . (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	lern	$$⊢{ℝ}^{*}=\mathrm{ran}\le$$

Proof

Step	Hyp	Ref	Expression
1		xrleid	$$⊢x\in {ℝ}^{*}\to x\le x$$
2		lerel	$$⊢\mathrm{Rel}\le$$
3	2	relelrni	$$⊢x\le x\to x\in \mathrm{ran}\le$$
4	1 3	syl	$$⊢x\in {ℝ}^{*}\to x\in \mathrm{ran}\le$$
5	4	ssriv	$$⊢{ℝ}^{*}\subseteq \mathrm{ran}\le$$
6		lerelxr	$$⊢\le \subseteq {ℝ}^{*}\times {ℝ}^{*}$$
7	6	rnssi	$$⊢\mathrm{ran}\le \subseteq \mathrm{ran}\left({ℝ}^{*}\times {ℝ}^{*}\right)$$
8		rnxpss	$$⊢\mathrm{ran}\left({ℝ}^{*}\times {ℝ}^{*}\right)\subseteq {ℝ}^{*}$$
9	7 8	sstri	$$⊢\mathrm{ran}\le \subseteq {ℝ}^{*}$$
10	5 9	eqssi	$$⊢{ℝ}^{*}=\mathrm{ran}\le$$