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