Step | Hyp | Ref
| Expression |
1 | | lhp0lt.s |
. . 3
⊢ < =
(lt‘𝐾) |
2 | | eqid 2823 |
. . 3
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
3 | | lhp0lt.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 1, 2, 3 | lhpexlt 37140 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ (Atoms‘𝐾)𝑝 < 𝑊) |
5 | | simp1l 1193 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝐾 ∈ HL) |
6 | | hlop 36500 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
7 | | eqid 2823 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
8 | | lhp0lt.z |
. . . . . . 7
⊢ 0 =
(0.‘𝐾) |
9 | 7, 8 | op0cl 36322 |
. . . . . 6
⊢ (𝐾 ∈ OP → 0 ∈
(Base‘𝐾)) |
10 | 5, 6, 9 | 3syl 18 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 ∈ (Base‘𝐾)) |
11 | 7, 2 | atbase 36427 |
. . . . . 6
⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ (Base‘𝐾)) |
12 | 11 | 3ad2ant2 1130 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑝 ∈ (Base‘𝐾)) |
13 | | simp2 1133 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑝 ∈ (Atoms‘𝐾)) |
14 | | eqid 2823 |
. . . . . . 7
⊢ ( ⋖
‘𝐾) = ( ⋖
‘𝐾) |
15 | 8, 14, 2 | atcvr0 36426 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atoms‘𝐾)) → 0 ( ⋖ ‘𝐾)𝑝) |
16 | 5, 13, 15 | syl2anc 586 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 ( ⋖ ‘𝐾)𝑝) |
17 | 7, 1, 14 | cvrlt 36408 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 0 ∈
(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾)) ∧ 0 ( ⋖ ‘𝐾)𝑝) → 0 < 𝑝) |
18 | 5, 10, 12, 16, 17 | syl31anc 1369 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 < 𝑝) |
19 | | simp3 1134 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑝 < 𝑊) |
20 | | hlpos 36504 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
21 | 5, 20 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝐾 ∈ Poset) |
22 | | simp1r 1194 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑊 ∈ 𝐻) |
23 | 7, 3 | lhpbase 37136 |
. . . . . 6
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑊 ∈ (Base‘𝐾)) |
25 | 7, 1 | plttr 17582 |
. . . . 5
⊢ ((𝐾 ∈ Poset ∧ ( 0 ∈
(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (( 0 < 𝑝 ∧ 𝑝 < 𝑊) → 0 < 𝑊)) |
26 | 21, 10, 12, 24, 25 | syl13anc 1368 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → (( 0 < 𝑝 ∧ 𝑝 < 𝑊) → 0 < 𝑊)) |
27 | 18, 19, 26 | mp2and 697 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 < 𝑊) |
28 | 27 | rexlimdv3a 3288 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (∃𝑝 ∈ (Atoms‘𝐾)𝑝 < 𝑊 → 0 < 𝑊)) |
29 | 4, 28 | mpd 15 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 < 𝑊) |