Step | Hyp | Ref
| Expression |
1 | | ovex 7216 |
. . . 4
⊢ (0[,]1)
∈ V |
2 | | chex 29174 |
. . . 4
⊢
Cℋ ∈ V |
3 | 1, 2 | elmap 8494 |
. . 3
⊢ (𝑆 ∈ ((0[,]1)
↑m Cℋ ) ↔ 𝑆: Cℋ
⟶(0[,]1)) |
4 | 3 | anbi1i 627 |
. 2
⊢ ((𝑆 ∈ ((0[,]1)
↑m Cℋ ) ∧ ((𝑆‘ ℋ) = 1 ∧
∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))))) ↔ (𝑆: Cℋ
⟶(0[,]1) ∧ ((𝑆‘ ℋ) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))))) |
5 | | fveq1 6686 |
. . . . 5
⊢ (𝑓 = 𝑆 → (𝑓‘ ℋ) = (𝑆‘ ℋ)) |
6 | 5 | eqeq1d 2741 |
. . . 4
⊢ (𝑓 = 𝑆 → ((𝑓‘ ℋ) = 1 ↔ (𝑆‘ ℋ) =
1)) |
7 | | fveq1 6686 |
. . . . . . 7
⊢ (𝑓 = 𝑆 → (𝑓‘(𝑥 ∨ℋ 𝑦)) = (𝑆‘(𝑥 ∨ℋ 𝑦))) |
8 | | fveq1 6686 |
. . . . . . . 8
⊢ (𝑓 = 𝑆 → (𝑓‘𝑥) = (𝑆‘𝑥)) |
9 | | fveq1 6686 |
. . . . . . . 8
⊢ (𝑓 = 𝑆 → (𝑓‘𝑦) = (𝑆‘𝑦)) |
10 | 8, 9 | oveq12d 7201 |
. . . . . . 7
⊢ (𝑓 = 𝑆 → ((𝑓‘𝑥) + (𝑓‘𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))) |
11 | 7, 10 | eqeq12d 2755 |
. . . . . 6
⊢ (𝑓 = 𝑆 → ((𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦)) ↔ (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))) |
12 | 11 | imbi2d 344 |
. . . . 5
⊢ (𝑓 = 𝑆 → ((𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))) ↔ (𝑥 ⊆ (⊥‘𝑦) → (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))))) |
13 | 12 | 2ralbidv 3112 |
. . . 4
⊢ (𝑓 = 𝑆 → (∀𝑥 ∈ Cℋ
∀𝑦 ∈
Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))) ↔ ∀𝑥 ∈ Cℋ
∀𝑦 ∈
Cℋ (𝑥 ⊆ (⊥‘𝑦) → (𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))))) |
14 | 6, 13 | anbi12d 634 |
. . 3
⊢ (𝑓 = 𝑆 → (((𝑓‘ ℋ) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦)))) ↔ ((𝑆‘ ℋ) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))))) |
15 | | df-st 30159 |
. . 3
⊢ States =
{𝑓 ∈ ((0[,]1)
↑m Cℋ ) ∣ ((𝑓‘ ℋ) = 1 ∧
∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑓‘(𝑥 ∨ℋ 𝑦)) = ((𝑓‘𝑥) + (𝑓‘𝑦))))} |
16 | 14, 15 | elrab2 3596 |
. 2
⊢ (𝑆 ∈ States ↔ (𝑆 ∈ ((0[,]1)
↑m Cℋ ) ∧ ((𝑆‘ ℋ) = 1 ∧
∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))))) |
17 | | 3anass 1096 |
. 2
⊢ ((𝑆:
Cℋ ⟶(0[,]1) ∧ (𝑆‘ ℋ) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))) ↔ (𝑆: Cℋ
⟶(0[,]1) ∧ ((𝑆‘ ℋ) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦)))))) |
18 | 4, 16, 17 | 3bitr4i 306 |
1
⊢ (𝑆 ∈ States ↔ (𝑆:
Cℋ ⟶(0[,]1) ∧ (𝑆‘ ℋ) = 1 ∧ ∀𝑥 ∈
Cℋ ∀𝑦 ∈ Cℋ
(𝑥 ⊆
(⊥‘𝑦) →
(𝑆‘(𝑥 ∨ℋ 𝑦)) = ((𝑆‘𝑥) + (𝑆‘𝑦))))) |