Metamath Proof Explorer


Theorem sticl

Description: [ 0 , 1 ] closure of the value of a state. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion sticl S States A C S A 0 1

Proof

Step Hyp Ref Expression
1 isst S States S : C 0 1 S = 1 x C y C x y S x y = S x + S y
2 1 simp1bi S States S : C 0 1
3 ffvelrn S : C 0 1 A C S A 0 1
4 3 ex S : C 0 1 A C S A 0 1
5 2 4 syl S States A C S A 0 1