Theorem ledm

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

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

Proof

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