Metamath Proof Explorer


Theorem stcl

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 ) )

Proof

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 ) )