Metamath Proof Explorer

Theorem hlhgt2

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

Ref Expression
Hypotheses hlhgt4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
hlhgt4.s ⊢ < = ( lt ‘ 𝐾 )
hlhgt4.z ⊢ 0 = ( 0. ‘ 𝐾 )
hlhgt4.u ⊢ 1 = ( 1. ‘ 𝐾 )
Assertion hlhgt2 ( 𝐾 ∈ 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 1 2 3 4 hlhgt4 ⊢ ( 𝐾 ∈ HL → ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧 ∧ 𝑧 < 1 ) ) )
6 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
7 6 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ Poset )
8 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
9 8 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ OP )
10 1 3 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )
11 9 10 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 0 ∈ 𝐵 )
12 simpllr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
13 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
14 1 2 plttr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) → 0 < 𝑥 ) )
15 7 11 12 13 14 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) → 0 < 𝑥 ) )
16 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
17 1 4 op1cl ⊢ ( 𝐾 ∈ OP → 1 ∈ 𝐵 )
18 9 17 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 1 ∈ 𝐵 )
19 1 2 plttr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) ) → ( ( 𝑥 < 𝑧 ∧ 𝑧 < 1 ) → 𝑥 < 1 ) )
20 7 13 16 18 19 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 < 𝑧 ∧ 𝑧 < 1 ) → 𝑥 < 1 ) )
21 15 20 anim12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧 ∧ 𝑧 < 1 ) ) → ( 0 < 𝑥 ∧ 𝑥 < 1 ) ) )
22 21 rexlimdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧 ∧ 𝑧 < 1 ) ) → ( 0 < 𝑥 ∧ 𝑥 < 1 ) ) )
23 22 reximdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧 ∧ 𝑧 < 1 ) ) → ∃ 𝑥 ∈ 𝐵 ( 0 < 𝑥 ∧ 𝑥 < 1 ) ) )
24 23 rexlimdva ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑦 ∧ 𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧 ∧ 𝑧 < 1 ) ) → ∃ 𝑥 ∈ 𝐵 ( 0 < 𝑥 ∧ 𝑥 < 1 ) ) )
25 5 24 mpd ⊢ ( 𝐾 ∈ HL → ∃ 𝑥 ∈ 𝐵 ( 0 < 𝑥 ∧ 𝑥 < 1 ) )