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 B = Base K
hlhgt4.s < ˙ = < K
hlhgt4.z 0 ˙ = 0. K
hlhgt4.u 1 ˙ = 1. K
Assertion hlhgt2 K HL x B 0 ˙ < ˙ x x < ˙ 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 1 2 3 4 hlhgt4 K HL y B x B z B 0 ˙ < ˙ y y < ˙ x x < ˙ z z < ˙ 1 ˙
6 hlpos K HL K Poset
7 6 ad3antrrr K HL y B x B z B K Poset
8 hlop K HL K OP
9 8 ad3antrrr K HL y B x B z B K OP
10 1 3 op0cl K OP 0 ˙ B
11 9 10 syl K HL y B x B z B 0 ˙ B
12 simpllr K HL y B x B z B y B
13 simplr K HL y B x B z B x B
14 1 2 plttr K Poset 0 ˙ B y B x B 0 ˙ < ˙ y y < ˙ x 0 ˙ < ˙ x
15 7 11 12 13 14 syl13anc K HL y B x B z B 0 ˙ < ˙ y y < ˙ x 0 ˙ < ˙ x
16 simpr K HL y B x B z B z B
17 1 4 op1cl K OP 1 ˙ B
18 9 17 syl K HL y B x B z B 1 ˙ B
19 1 2 plttr K Poset x B z B 1 ˙ B x < ˙ z z < ˙ 1 ˙ x < ˙ 1 ˙
20 7 13 16 18 19 syl13anc K HL y B x B z B x < ˙ z z < ˙ 1 ˙ x < ˙ 1 ˙
21 15 20 anim12d K HL y B x B z B 0 ˙ < ˙ y y < ˙ x x < ˙ z z < ˙ 1 ˙ 0 ˙ < ˙ x x < ˙ 1 ˙
22 21 rexlimdva K HL y B x B z B 0 ˙ < ˙ y y < ˙ x x < ˙ z z < ˙ 1 ˙ 0 ˙ < ˙ x x < ˙ 1 ˙
23 22 reximdva K HL y B x B z B 0 ˙ < ˙ y y < ˙ x x < ˙ z z < ˙ 1 ˙ x B 0 ˙ < ˙ x x < ˙ 1 ˙
24 23 rexlimdva K HL y B x B z B 0 ˙ < ˙ y y < ˙ x x < ˙ z z < ˙ 1 ˙ x B 0 ˙ < ˙ x x < ˙ 1 ˙
25 5 24 mpd K HL x B 0 ˙ < ˙ x x < ˙ 1 ˙