Description: The range of <_ is RR* . (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 3-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lern | ⊢ ℝ* = ran ≤ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xrleid | ⊢ ( 𝑥 ∈ ℝ* → 𝑥 ≤ 𝑥 ) | |
| 2 | lerel | ⊢ Rel ≤ | |
| 3 | 2 | relelrni | ⊢ ( 𝑥 ≤ 𝑥 → 𝑥 ∈ ran ≤ ) |
| 4 | 1 3 | syl | ⊢ ( 𝑥 ∈ ℝ* → 𝑥 ∈ ran ≤ ) |
| 5 | 4 | ssriv | ⊢ ℝ* ⊆ ran ≤ |
| 6 | lerelxr | ⊢ ≤ ⊆ ( ℝ* × ℝ* ) | |
| 7 | 6 | rnssi | ⊢ ran ≤ ⊆ ran ( ℝ* × ℝ* ) |
| 8 | rnxpss | ⊢ ran ( ℝ* × ℝ* ) ⊆ ℝ* | |
| 9 | 7 8 | sstri | ⊢ ran ≤ ⊆ ℝ* |
| 10 | 5 9 | eqssi | ⊢ ℝ* = ran ≤ |