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ℋ ( 𝑥 ⊆ ( ⊥ ‘ 𝑦 ) → ( 𝑆 ‘ ( 𝑥 ∨ℋ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) + ( 𝑆 ‘ 𝑦 ) ) ) ) )