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 ⊢ < ˙ = < K
hl0lt1.z ⊢ 0 ˙ = 0. ⁡ K
hl0lt1.u ⊢ 1 ˙ = 1. ⁡ K
Assertion hl0lt1N ⊢ K ∈ HL → 0 ˙ < ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 hl0lt1.s ⊢ < ˙ = < 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 ∈ HL → ∃ x ∈ Base K 0 ˙ < ˙ x ∧ x < ˙ 1 ˙
6 hlpos ⊢ K ∈ HL → K ∈ Poset
7 6 adantr ⊢ K ∈ HL ∧ x ∈ Base K → K ∈ Poset
8 hlop ⊢ K ∈ HL → K ∈ OP
9 8 adantr ⊢ K ∈ HL ∧ x ∈ Base K → K ∈ OP
10 4 2 op0cl ⊢ K ∈ OP → 0 ˙ ∈ Base K
11 9 10 syl ⊢ K ∈ HL ∧ x ∈ Base K → 0 ˙ ∈ Base K
12 simpr ⊢ K ∈ HL ∧ x ∈ Base K → x ∈ Base K
13 4 3 op1cl ⊢ K ∈ OP → 1 ˙ ∈ Base K
14 9 13 syl ⊢ K ∈ HL ∧ x ∈ Base K → 1 ˙ ∈ Base K
15 4 1 plttr ⊢ K ∈ Poset ∧ 0 ˙ ∈ Base K ∧ x ∈ Base K ∧ 1 ˙ ∈ Base K → 0 ˙ < ˙ x ∧ x < ˙ 1 ˙ → 0 ˙ < ˙ 1 ˙
16 7 11 12 14 15 syl13anc ⊢ K ∈ HL ∧ x ∈ Base K → 0 ˙ < ˙ x ∧ x < ˙ 1 ˙ → 0 ˙ < ˙ 1 ˙
17 16 rexlimdva ⊢ K ∈ HL → ∃ x ∈ Base K 0 ˙ < ˙ x ∧ x < ˙ 1 ˙ → 0 ˙ < ˙ 1 ˙
18 5 17 mpd ⊢ K ∈ HL → 0 ˙ < ˙ 1 ˙