Description: The value of a state is less than or equal to one. (Contributed by NM, 24-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | stle1 | |- ( S e. States -> ( A e. CH -> ( S ` A ) <_ 1 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sticl | |- ( S e. States -> ( A e. CH -> ( S ` A ) e. ( 0 [,] 1 ) ) ) |
|
| 2 | elicc01 | |- ( ( S ` A ) e. ( 0 [,] 1 ) <-> ( ( S ` A ) e. RR /\ 0 <_ ( S ` A ) /\ ( S ` A ) <_ 1 ) ) |
|
| 3 | 2 | simp3bi | |- ( ( S ` A ) e. ( 0 [,] 1 ) -> ( S ` A ) <_ 1 ) |
| 4 | 1 3 | syl6 | |- ( S e. States -> ( A e. CH -> ( S ` A ) <_ 1 ) ) |