Metamath Proof Explorer

Theorem isst

Description: Property of a state. (Contributed by NM, 23-Oct-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion isst 
|- ( S e. States <-> ( S : CH --> ( 0 [,] 1 ) /\ ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( 0 [,] 1 ) e. _V
2 chex 
 |-  CH e. _V
3 1 2 elmap 
 |-  ( S e. ( ( 0 [,] 1 ) ^m CH ) <-> S : CH --> ( 0 [,] 1 ) )
4 3 anbi1i 
 |-  ( ( S e. ( ( 0 [,] 1 ) ^m CH ) /\ ( ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) ) <-> ( S : CH --> ( 0 [,] 1 ) /\ ( ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) ) )
5 fveq1 
 |-  ( f = S -> ( f ` ~H ) = ( S ` ~H ) )
6 5 eqeq1d 
 |-  ( f = S -> ( ( f ` ~H ) = 1 <-> ( S ` ~H ) = 1 ) )
7 fveq1 
 |-  ( f = S -> ( f ` ( x vH y ) ) = ( S ` ( x vH y ) ) )
8 fveq1 
 |-  ( f = S -> ( f ` x ) = ( S ` x ) )
9 fveq1 
 |-  ( f = S -> ( f ` y ) = ( S ` y ) )
10 8 9 oveq12d 
 |-  ( f = S -> ( ( f ` x ) + ( f ` y ) ) = ( ( S ` x ) + ( S ` y ) ) )
11 7 10 eqeq12d 
 |-  ( f = S -> ( ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) <-> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) )
12 11 imbi2d 
 |-  ( f = S -> ( ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) <-> ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) )
13 12 2ralbidv 
 |-  ( f = S -> ( A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) <-> A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) )
14 6 13 anbi12d 
 |-  ( f = S -> ( ( ( f ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) ) <-> ( ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) ) )
15 df-st 
 |-  States = { f e. ( ( 0 [,] 1 ) ^m CH ) | ( ( f ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( f ` ( x vH y ) ) = ( ( f ` x ) + ( f ` y ) ) ) ) }
16 14 15 elrab2 
 |-  ( S e. States <-> ( S e. ( ( 0 [,] 1 ) ^m CH ) /\ ( ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) ) )
17 3anass 
 |-  ( ( S : CH --> ( 0 [,] 1 ) /\ ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) <-> ( S : CH --> ( 0 [,] 1 ) /\ ( ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) ) )
18 4 16 17 3bitr4i 
 |-  ( S e. States <-> ( S : CH --> ( 0 [,] 1 ) /\ ( S ` ~H ) = 1 /\ A. x e. CH A. y e. CH ( x C_ ( _|_ ` y ) -> ( S ` ( x vH y ) ) = ( ( S ` x ) + ( S ` y ) ) ) ) )