Step |
Hyp |
Ref |
Expression |
1 |
|
large.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
ralnex |
⊢ ( ∀ 𝑓 ∈ States ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ¬ ∃ 𝑓 ∈ States ( 𝑓 ‘ 𝐴 ) = 1 ) |
3 |
|
ax-1ne0 |
⊢ 1 ≠ 0 |
4 |
3
|
neii |
⊢ ¬ 1 = 0 |
5 |
|
st0 |
⊢ ( 𝑓 ∈ States → ( 𝑓 ‘ 0ℋ ) = 0 ) |
6 |
5
|
eqeq1d |
⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ 0ℋ ) = 1 ↔ 0 = 1 ) ) |
7 |
|
eqcom |
⊢ ( 0 = 1 ↔ 1 = 0 ) |
8 |
6 7
|
bitrdi |
⊢ ( 𝑓 ∈ States → ( ( 𝑓 ‘ 0ℋ ) = 1 ↔ 1 = 0 ) ) |
9 |
4 8
|
mtbiri |
⊢ ( 𝑓 ∈ States → ¬ ( 𝑓 ‘ 0ℋ ) = 1 ) |
10 |
|
mtt |
⊢ ( ¬ ( 𝑓 ‘ 0ℋ ) = 1 → ( ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) ) ) |
11 |
9 10
|
syl |
⊢ ( 𝑓 ∈ States → ( ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) ) ) |
12 |
11
|
ralbiia |
⊢ ( ∀ 𝑓 ∈ States ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ ∀ 𝑓 ∈ States ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) ) |
13 |
|
h0elch |
⊢ 0ℋ ∈ Cℋ |
14 |
1 13
|
strb |
⊢ ( ∀ 𝑓 ∈ States ( ( 𝑓 ‘ 𝐴 ) = 1 → ( 𝑓 ‘ 0ℋ ) = 1 ) ↔ 𝐴 ⊆ 0ℋ ) |
15 |
1
|
chle0i |
⊢ ( 𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ ) |
16 |
12 14 15
|
3bitri |
⊢ ( ∀ 𝑓 ∈ States ¬ ( 𝑓 ‘ 𝐴 ) = 1 ↔ 𝐴 = 0ℋ ) |
17 |
2 16
|
bitr3i |
⊢ ( ¬ ∃ 𝑓 ∈ States ( 𝑓 ‘ 𝐴 ) = 1 ↔ 𝐴 = 0ℋ ) |
18 |
17
|
con1bii |
⊢ ( ¬ 𝐴 = 0ℋ ↔ ∃ 𝑓 ∈ States ( 𝑓 ‘ 𝐴 ) = 1 ) |