Description: Real closure of the value of a state. (Contributed by NM, 24-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | stcl | |- ( S e. States -> ( A e. CH -> ( S ` A ) e. RR ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sticl | |- ( S e. States -> ( A e. CH -> ( S ` A ) e. ( 0 [,] 1 ) ) ) |
|
2 | unitssre | |- ( 0 [,] 1 ) C_ RR |
|
3 | 2 | sseli | |- ( ( S ` A ) e. ( 0 [,] 1 ) -> ( S ` A ) e. RR ) |
4 | 1 3 | syl6 | |- ( S e. States -> ( A e. CH -> ( S ` A ) e. RR ) ) |