ledm

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

		Ref	Expression
	Assertion	ledm	$⊢ ℝ^{*} = dom \leq$

Step	Hyp	Ref	Expression
1		xrleid	$⊢ x \in ℝ^{*} \to x \leq x$
2		lerel	$⊢ Rel \leq$
3	2	releldmi	$⊢ x \leq x \to x \in dom \leq$
4	1 3	syl	$⊢ x \in ℝ^{*} \to x \in dom \leq$
5	4	ssriv	$⊢ ℝ^{*} \subseteq dom \leq$
6		lerelxr	$⊢ \leq \subseteq ℝ^{} \times ℝ^{}$
7		dmss	$⊢ \leq \subseteq ℝ^{} \times ℝ^{} \to dom \leq \subseteq dom (ℝ^{} \times ℝ^{})$
8	6 7	ax-mp	$⊢ dom \leq \subseteq dom (ℝ^{} \times ℝ^{})$
9		dmxpss	$⊢ dom (ℝ^{} \times ℝ^{}) \subseteq ℝ^{*}$
10	8 9	sstri	$⊢ dom \leq \subseteq ℝ^{*}$
11	5 10	eqssi	$⊢ ℝ^{*} = dom \leq$

Metamath Proof Explorer