lern

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

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

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

Metamath Proof Explorer