Description: The range of the indicator function is a subset of RR . (Contributed by Thierry Arnoux, 14-Aug-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | pr01ssre | ⊢ { 0 , 1 } ⊆ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re | ⊢ 0 ∈ ℝ | |
2 | 1re | ⊢ 1 ∈ ℝ | |
3 | prssi | ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → { 0 , 1 } ⊆ ℝ ) | |
4 | 1 2 3 | mp2an | ⊢ { 0 , 1 } ⊆ ℝ |