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. ) ) )