Description: A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlhgt4.b | |
|
hlhgt4.s | |
||
hlhgt4.z | |
||
hlhgt4.u | |
||
Assertion | hlhgt4 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlhgt4.b | |
|
2 | hlhgt4.s | |
|
3 | hlhgt4.z | |
|
4 | hlhgt4.u | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | 1 5 2 6 3 4 7 | ishlat2 | |
9 | simprr | |
|
10 | 8 9 | sylbi | |