This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 
|- .< = ( lt ` K )
hlhgt4.z 
|- .0. = ( 0. ` K )
hlhgt4.u 
|- .1. = ( 1. ` K )
Assertion hlhgt4 
|- ( K e. HL -> E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) )

Proof

Step Hyp Ref Expression
1 hlhgt4.b 
 |-  B = ( Base ` K )
2 hlhgt4.s 
 |-  .< = ( lt ` K )
3 hlhgt4.z 
 |-  .0. = ( 0. ` K )
4 hlhgt4.u 
 |-  .1. = ( 1. ` K )
5 eqid 
 |-  ( le ` K ) = ( le ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 1 5 2 6 3 4 7 ishlat2 
 |-  ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ ( A. x e. ( Atoms ` K ) A. y e. ( Atoms ` K ) ( ( x =/= y -> E. z e. ( Atoms ` K ) ( z =/= x /\ z =/= y /\ z ( le ` K ) ( x ( join ` K ) y ) ) ) /\ A. z e. B ( ( -. x ( le ` K ) z /\ x ( le ` K ) ( z ( join ` K ) y ) ) -> y ( le ` K ) ( z ( join ` K ) x ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )
9 simprr 
 |-  ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ ( A. x e. ( Atoms ` K ) A. y e. ( Atoms ` K ) ( ( x =/= y -> E. z e. ( Atoms ` K ) ( z =/= x /\ z =/= y /\ z ( le ` K ) ( x ( join ` K ) y ) ) ) /\ A. z e. B ( ( -. x ( le ` K ) z /\ x ( le ` K ) ( z ( join ` K ) y ) ) -> y ( le ` K ) ( z ( join ` K ) x ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) -> E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) )
10 8 9 sylbi 
 |-  ( K e. HL -> E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) )