Step | Hyp | Ref
| Expression |
1 | | lhp0lt.s |
. . 3
⊢ < =
(lt‘𝐾) |
2 | | eqid 2798 |
. . 3
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
3 | | lhp0lt.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 1, 2, 3 | lhpexlt 37298 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ (Atoms‘𝐾)𝑝 < 𝑊) |
5 | | simp1l 1194 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝐾 ∈ HL) |
6 | | hlop 36658 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
7 | | eqid 2798 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
8 | | lhp0lt.z |
. . . . . . 7
⊢ 0 =
(0.‘𝐾) |
9 | 7, 8 | op0cl 36480 |
. . . . . 6
⊢ (𝐾 ∈ OP → 0 ∈
(Base‘𝐾)) |
10 | 5, 6, 9 | 3syl 18 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 ∈ (Base‘𝐾)) |
11 | 7, 2 | atbase 36585 |
. . . . . 6
⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ (Base‘𝐾)) |
12 | 11 | 3ad2ant2 1131 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑝 ∈ (Base‘𝐾)) |
13 | | simp2 1134 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑝 ∈ (Atoms‘𝐾)) |
14 | | eqid 2798 |
. . . . . . 7
⊢ ( ⋖
‘𝐾) = ( ⋖
‘𝐾) |
15 | 8, 14, 2 | atcvr0 36584 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atoms‘𝐾)) → 0 ( ⋖ ‘𝐾)𝑝) |
16 | 5, 13, 15 | syl2anc 587 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 ( ⋖ ‘𝐾)𝑝) |
17 | 7, 1, 14 | cvrlt 36566 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 0 ∈
(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾)) ∧ 0 ( ⋖ ‘𝐾)𝑝) → 0 < 𝑝) |
18 | 5, 10, 12, 16, 17 | syl31anc 1370 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 < 𝑝) |
19 | | simp3 1135 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑝 < 𝑊) |
20 | | hlpos 36662 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
21 | 5, 20 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝐾 ∈ Poset) |
22 | | simp1r 1195 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑊 ∈ 𝐻) |
23 | 7, 3 | lhpbase 37294 |
. . . . . 6
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 𝑊 ∈ (Base‘𝐾)) |
25 | 7, 1 | plttr 17572 |
. . . . 5
⊢ ((𝐾 ∈ Poset ∧ ( 0 ∈
(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (( 0 < 𝑝 ∧ 𝑝 < 𝑊) → 0 < 𝑊)) |
26 | 21, 10, 12, 24, 25 | syl13anc 1369 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → (( 0 < 𝑝 ∧ 𝑝 < 𝑊) → 0 < 𝑊)) |
27 | 18, 19, 26 | mp2and 698 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑝 ∈ (Atoms‘𝐾) ∧ 𝑝 < 𝑊) → 0 < 𝑊) |
28 | 27 | rexlimdv3a 3245 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (∃𝑝 ∈ (Atoms‘𝐾)𝑝 < 𝑊 → 0 < 𝑊)) |
29 | 4, 28 | mpd 15 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 < 𝑊) |