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

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 )