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

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