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	⊢ ℝ* = dom ≤

Proof

Step	Hyp	Ref	Expression
1		xrleid	⊢ ( 𝑥 ∈ ℝ* → 𝑥 ≤ 𝑥 )
2		lerel	⊢ Rel ≤
3	2	releldmi	⊢ ( 𝑥 ≤ 𝑥 → 𝑥 ∈ dom ≤ )
4	1 3	syl	⊢ ( 𝑥 ∈ ℝ* → 𝑥 ∈ dom ≤ )
5	4	ssriv	⊢ ℝ* ⊆ dom ≤
6		lerelxr	⊢ ≤ ⊆ ( ℝ* × ℝ* )
7		dmss	⊢ ( ≤ ⊆ ( ℝ* × ℝ* ) → dom ≤ ⊆ dom ( ℝ* × ℝ* ) )
8	6 7	ax-mp	⊢ dom ≤ ⊆ dom ( ℝ* × ℝ* )
9		dmxpss	⊢ dom ( ℝ* × ℝ* ) ⊆ ℝ*
10	8 9	sstri	⊢ dom ≤ ⊆ ℝ*
11	5 10	eqssi	⊢ ℝ* = dom ≤