Theorem hlhgt4

Description: A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011)

	Ref	Expression
Hypotheses	hlhgt4.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	hlhgt4.s	⊢ < = ( lt ‘ 𝐾 )
	hlhgt4.z	⊢ 0 = ( 0. ‘ 𝐾 )
	hlhgt4.u	⊢ 1 = ( 1. ‘ 𝐾 )
Assertion	hlhgt4	⊢ ( 𝐾 ∈ HL → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlhgt4.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		hlhgt4.s	⊢ < = ( lt ‘ 𝐾 )
3		hlhgt4.z	⊢ 0 = ( 0. ‘ 𝐾 )
4		hlhgt4.u	⊢ 1 = ( 1. ‘ 𝐾 )
5		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8	1 5 2 6 3 4 7	ishlat2	⊢ ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( ∀ 𝑥 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝐾 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ( le ‘ 𝐾 ) 𝑧 ∧ 𝑥 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑦 ) ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑥 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
9		simprr	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( ∀ 𝑥 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝐾 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ( le ‘ 𝐾 ) 𝑧 ∧ 𝑥 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑦 ) ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑧 ( join ‘ 𝐾 ) 𝑥 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )
10	8 9	sylbi	⊢ ( 𝐾 ∈ HL → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )