Metamath Proof Explorer

Theorem hl0lt1N

Description: Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011) (New usage is discouraged.)

Ref Expression
Hypotheses hl0lt1.s 
|- .< = ( lt ` K )
hl0lt1.z 
|- .0. = ( 0. ` K )
hl0lt1.u 
|- .1. = ( 1. ` K )
Assertion hl0lt1N 
|- ( K e. HL -> .0. .< .1. )

Proof

Step Hyp Ref Expression
1 hl0lt1.s 
 |-  .< = ( lt ` K )
2 hl0lt1.z 
 |-  .0. = ( 0. ` K )
3 hl0lt1.u 
 |-  .1. = ( 1. ` K )
4 eqid 
 |-  ( Base ` K ) = ( Base ` K )
5 4 1 2 3 hlhgt2 
 |-  ( K e. HL -> E. x e. ( Base ` K ) ( .0. .< x /\ x .< .1. ) )
6 hlpos 
 |-  ( K e. HL -> K e. Poset )
7 6 adantr 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> K e. Poset )
8 hlop 
 |-  ( K e. HL -> K e. OP )
9 8 adantr 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> K e. OP )
10 4 2 op0cl 
 |-  ( K e. OP -> .0. e. ( Base ` K ) )
11 9 10 syl 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> .0. e. ( Base ` K ) )
12 simpr 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> x e. ( Base ` K ) )
13 4 3 op1cl 
 |-  ( K e. OP -> .1. e. ( Base ` K ) )
14 9 13 syl 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> .1. e. ( Base ` K ) )
15 4 1 plttr 
 |-  ( ( K e. Poset /\ ( .0. e. ( Base ` K ) /\ x e. ( Base ` K ) /\ .1. e. ( Base ` K ) ) ) -> ( ( .0. .< x /\ x .< .1. ) -> .0. .< .1. ) )
16 7 11 12 14 15 syl13anc 
 |-  ( ( K e. HL /\ x e. ( Base ` K ) ) -> ( ( .0. .< x /\ x .< .1. ) -> .0. .< .1. ) )
17 16 rexlimdva 
 |-  ( K e. HL -> ( E. x e. ( Base ` K ) ( .0. .< x /\ x .< .1. ) -> .0. .< .1. ) )
18 5 17 mpd 
 |-  ( K e. HL -> .0. .< .1. )