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. )