This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≤