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