# 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 ( 𝑆 ∈ States ↔ ( 𝑆 : C ⟶ ( 0 [,] 1 ) ∧ ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 ovex ( 0 [,] 1 ) ∈ V
2 chex C ∈ V
3 1 2 elmap ( 𝑆 ∈ ( ( 0 [,] 1 ) ↑m C ) ↔ 𝑆 : C ⟶ ( 0 [,] 1 ) )
4 3 anbi1i ( ( 𝑆 ∈ ( ( 0 [,] 1 ) ↑m C ) ∧ ( ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) ) ↔ ( 𝑆 : C ⟶ ( 0 [,] 1 ) ∧ ( ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) ) )
5 fveq1 ( 𝑓 = 𝑆 → ( 𝑓 ‘ ℋ ) = ( 𝑆 ‘ ℋ ) )
6 5 eqeq1d ( 𝑓 = 𝑆 → ( ( 𝑓 ‘ ℋ ) = 1 ↔ ( 𝑆 ‘ ℋ ) = 1 ) )
7 fveq1 ( 𝑓 = 𝑆 → ( 𝑓 ‘ ( 𝑥 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝑦 ) ) )
8 fveq1 ( 𝑓 = 𝑆 → ( 𝑓𝑥 ) = ( 𝑆𝑥 ) )
9 fveq1 ( 𝑓 = 𝑆 → ( 𝑓𝑦 ) = ( 𝑆𝑦 ) )
10 8 9 oveq12d ( 𝑓 = 𝑆 → ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) )
11 7 10 eqeq12d ( 𝑓 = 𝑆 → ( ( 𝑓 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ↔ ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) )
12 11 imbi2d ( 𝑓 = 𝑆 → ( ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑓 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ↔ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) )
13 12 2ralbidv ( 𝑓 = 𝑆 → ( ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑓 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ↔ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) )
14 6 13 anbi12d ( 𝑓 = 𝑆 → ( ( ( 𝑓 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑓 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) ↔ ( ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) ) )
15 df-st States = { 𝑓 ∈ ( ( 0 [,] 1 ) ↑m C ) ∣ ( ( 𝑓 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑓 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑓𝑥 ) + ( 𝑓𝑦 ) ) ) ) }
16 14 15 elrab2 ( 𝑆 ∈ States ↔ ( 𝑆 ∈ ( ( 0 [,] 1 ) ↑m C ) ∧ ( ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) ) )
17 3anass ( ( 𝑆 : C ⟶ ( 0 [,] 1 ) ∧ ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) ↔ ( 𝑆 : C ⟶ ( 0 [,] 1 ) ∧ ( ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) ) )
18 4 16 17 3bitr4i ( 𝑆 ∈ States ↔ ( 𝑆 : C ⟶ ( 0 [,] 1 ) ∧ ( 𝑆 ‘ ℋ ) = 1 ∧ ∀ 𝑥C𝑦C ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 𝑦 ) ) = ( ( 𝑆𝑥 ) + ( 𝑆𝑦 ) ) ) ) )