Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Hilbert lattices
hlhgt4
Next ⟩
hlhgt2
Metamath Proof Explorer
Ascii
Unicode
Theorem
hlhgt4
Description:
A Hilbert lattice has a height of at least 4.
(Contributed by
NM
, 4-Dec-2011)
Ref
Expression
Hypotheses
hlhgt4.b
⊢
B
=
Base
K
hlhgt4.s
⊢
<
˙
=
<
K
hlhgt4.z
⊢
0
˙
=
0.
⁡
K
hlhgt4.u
⊢
1
˙
=
1.
⁡
K
Assertion
hlhgt4
⊢
K
∈
HL
→
∃
x
∈
B
∃
y
∈
B
∃
z
∈
B
0
˙
<
˙
x
∧
x
<
˙
y
∧
y
<
˙
z
∧
z
<
˙
1
˙
Proof
Step
Hyp
Ref
Expression
1
hlhgt4.b
⊢
B
=
Base
K
2
hlhgt4.s
⊢
<
˙
=
<
K
3
hlhgt4.z
⊢
0
˙
=
0.
⁡
K
4
hlhgt4.u
⊢
1
˙
=
1.
⁡
K
5
eqid
⊢
≤
K
=
≤
K
6
eqid
⊢
join
⁡
K
=
join
⁡
K
7
eqid
⊢
Atoms
⁡
K
=
Atoms
⁡
K
8
1
5
2
6
3
4
7
ishlat2
⊢
K
∈
HL
↔
K
∈
OML
∧
K
∈
CLat
∧
K
∈
AtLat
∧
∀
x
∈
Atoms
⁡
K
∀
y
∈
Atoms
⁡
K
x
≠
y
→
∃
z
∈
Atoms
⁡
K
z
≠
x
∧
z
≠
y
∧
z
≤
K
x
join
⁡
K
y
∧
∀
z
∈
B
¬
x
≤
K
z
∧
x
≤
K
z
join
⁡
K
y
→
y
≤
K
z
join
⁡
K
x
∧
∃
x
∈
B
∃
y
∈
B
∃
z
∈
B
0
˙
<
˙
x
∧
x
<
˙
y
∧
y
<
˙
z
∧
z
<
˙
1
˙
9
simprr
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
AtLat
∧
∀
x
∈
Atoms
⁡
K
∀
y
∈
Atoms
⁡
K
x
≠
y
→
∃
z
∈
Atoms
⁡
K
z
≠
x
∧
z
≠
y
∧
z
≤
K
x
join
⁡
K
y
∧
∀
z
∈
B
¬
x
≤
K
z
∧
x
≤
K
z
join
⁡
K
y
→
y
≤
K
z
join
⁡
K
x
∧
∃
x
∈
B
∃
y
∈
B
∃
z
∈
B
0
˙
<
˙
x
∧
x
<
˙
y
∧
y
<
˙
z
∧
z
<
˙
1
˙
→
∃
x
∈
B
∃
y
∈
B
∃
z
∈
B
0
˙
<
˙
x
∧
x
<
˙
y
∧
y
<
˙
z
∧
z
<
˙
1
˙
10
8
9
sylbi
⊢
K
∈
HL
→
∃
x
∈
B
∃
y
∈
B
∃
z
∈
B
0
˙
<
˙
x
∧
x
<
˙
y
∧
y
<
˙
z
∧
z
<
˙
1
˙