Metamath Proof Explorer


Theorem stle1

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 ( 𝑆 ∈ States → ( 𝐴C → ( 𝑆𝐴 ) ≤ 1 ) )

Proof

Step Hyp Ref Expression
1 sticl ( 𝑆 ∈ States → ( 𝐴C → ( 𝑆𝐴 ) ∈ ( 0 [,] 1 ) ) )
2 elicc01 ( ( 𝑆𝐴 ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝑆𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝑆𝐴 ) ∧ ( 𝑆𝐴 ) ≤ 1 ) )
3 2 simp3bi ( ( 𝑆𝐴 ) ∈ ( 0 [,] 1 ) → ( 𝑆𝐴 ) ≤ 1 )
4 1 3 syl6 ( 𝑆 ∈ States → ( 𝐴C → ( 𝑆𝐴 ) ≤ 1 ) )