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 ‘ 𝐾 )
hl0lt1.z 0 = ( 0. ‘ 𝐾 )
hl0lt1.u 1 = ( 1. ‘ 𝐾 )
Assertion hl0lt1N ( 𝐾 ∈ HL → 0 < 1 )

Proof

Step Hyp Ref Expression
1 hl0lt1.s < = ( lt ‘ 𝐾 )
2 hl0lt1.z 0 = ( 0. ‘ 𝐾 )
3 hl0lt1.u 1 = ( 1. ‘ 𝐾 )
4 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 4 1 2 3 hlhgt2 ( 𝐾 ∈ HL → ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 0 < 𝑥𝑥 < 1 ) )
6 hlpos ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
7 6 adantr ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ Poset )
8 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
9 8 adantr ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ OP )
10 4 2 op0cl ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
11 9 10 syl ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 0 ∈ ( Base ‘ 𝐾 ) )
12 simpr ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
13 4 3 op1cl ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) )
14 9 13 syl ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 1 ∈ ( Base ‘ 𝐾 ) )
15 4 1 plttr ( ( 𝐾 ∈ Poset ∧ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 1 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 0 < 𝑥𝑥 < 1 ) → 0 < 1 ) )
16 7 11 12 14 15 syl13anc ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0 < 𝑥𝑥 < 1 ) → 0 < 1 ) )
17 16 rexlimdva ( 𝐾 ∈ HL → ( ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 0 < 𝑥𝑥 < 1 ) → 0 < 1 ) )
18 5 17 mpd ( 𝐾 ∈ HL → 0 < 1 )