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 } C_ RR |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re | |- 0 e. RR |
|
2 | 1re | |- 1 e. RR |
|
3 | prssi | |- ( ( 0 e. RR /\ 1 e. RR ) -> { 0 , 1 } C_ RR ) |
|
4 | 1 2 3 | mp2an | |- { 0 , 1 } C_ RR |