Step |
Hyp |
Ref |
Expression |
1 |
|
large.1 |
|- A e. CH |
2 |
|
ralnex |
|- ( A. f e. States -. ( f ` A ) = 1 <-> -. E. f e. States ( f ` A ) = 1 ) |
3 |
|
ax-1ne0 |
|- 1 =/= 0 |
4 |
3
|
neii |
|- -. 1 = 0 |
5 |
|
st0 |
|- ( f e. States -> ( f ` 0H ) = 0 ) |
6 |
5
|
eqeq1d |
|- ( f e. States -> ( ( f ` 0H ) = 1 <-> 0 = 1 ) ) |
7 |
|
eqcom |
|- ( 0 = 1 <-> 1 = 0 ) |
8 |
6 7
|
bitrdi |
|- ( f e. States -> ( ( f ` 0H ) = 1 <-> 1 = 0 ) ) |
9 |
4 8
|
mtbiri |
|- ( f e. States -> -. ( f ` 0H ) = 1 ) |
10 |
|
mtt |
|- ( -. ( f ` 0H ) = 1 -> ( -. ( f ` A ) = 1 <-> ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) ) ) |
11 |
9 10
|
syl |
|- ( f e. States -> ( -. ( f ` A ) = 1 <-> ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) ) ) |
12 |
11
|
ralbiia |
|- ( A. f e. States -. ( f ` A ) = 1 <-> A. f e. States ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) ) |
13 |
|
h0elch |
|- 0H e. CH |
14 |
1 13
|
strb |
|- ( A. f e. States ( ( f ` A ) = 1 -> ( f ` 0H ) = 1 ) <-> A C_ 0H ) |
15 |
1
|
chle0i |
|- ( A C_ 0H <-> A = 0H ) |
16 |
12 14 15
|
3bitri |
|- ( A. f e. States -. ( f ` A ) = 1 <-> A = 0H ) |
17 |
2 16
|
bitr3i |
|- ( -. E. f e. States ( f ` A ) = 1 <-> A = 0H ) |
18 |
17
|
con1bii |
|- ( -. A = 0H <-> E. f e. States ( f ` A ) = 1 ) |