| Step | Hyp | Ref
| Expression |
| 1 | | simp2 1138 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) → 𝑋 ∈ 𝑁) |
| 2 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 3 | | eqid 2737 |
. . . . . 6
⊢ ( ⋖
‘𝐾) = ( ⋖
‘𝐾) |
| 4 | | llnnleat.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
| 5 | | llnnleat.n |
. . . . . 6
⊢ 𝑁 = (LLines‘𝐾) |
| 6 | 2, 3, 4, 5 | islln 39508 |
. . . . 5
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑁 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ 𝐴 𝑞( ⋖ ‘𝐾)𝑋))) |
| 7 | 6 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) → (𝑋 ∈ 𝑁 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ 𝐴 𝑞( ⋖ ‘𝐾)𝑋))) |
| 8 | 1, 7 | mpbid 232 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ 𝐴 𝑞( ⋖ ‘𝐾)𝑋)) |
| 9 | 8 | simprd 495 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) → ∃𝑞 ∈ 𝐴 𝑞( ⋖ ‘𝐾)𝑋) |
| 10 | | simp11 1204 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝐾 ∈ HL) |
| 11 | | hlatl 39361 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
| 12 | 10, 11 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝐾 ∈ AtLat) |
| 13 | | simp2 1138 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑞 ∈ 𝐴) |
| 14 | | simp13 1206 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑃 ∈ 𝐴) |
| 15 | | eqid 2737 |
. . . . . 6
⊢
(lt‘𝐾) =
(lt‘𝐾) |
| 16 | 15, 4 | atnlt 39314 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑞 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → ¬ 𝑞(lt‘𝐾)𝑃) |
| 17 | 12, 13, 14, 16 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → ¬ 𝑞(lt‘𝐾)𝑃) |
| 18 | 2, 4 | atbase 39290 |
. . . . . . 7
⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ (Base‘𝐾)) |
| 19 | 18 | 3ad2ant2 1135 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑞 ∈ (Base‘𝐾)) |
| 20 | | simp12 1205 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑋 ∈ 𝑁) |
| 21 | 2, 5 | llnbase 39511 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑁 → 𝑋 ∈ (Base‘𝐾)) |
| 22 | 20, 21 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑋 ∈ (Base‘𝐾)) |
| 23 | | simp3 1139 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑞( ⋖ ‘𝐾)𝑋) |
| 24 | 2, 15, 3 | cvrlt 39271 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑞 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑞(lt‘𝐾)𝑋) |
| 25 | 10, 19, 22, 23, 24 | syl31anc 1375 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑞(lt‘𝐾)𝑋) |
| 26 | | hlpos 39367 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
| 27 | 10, 26 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝐾 ∈ Poset) |
| 28 | 2, 4 | atbase 39290 |
. . . . . . 7
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
| 29 | 14, 28 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → 𝑃 ∈ (Base‘𝐾)) |
| 30 | | llnnleat.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
| 31 | 2, 30, 15 | pltletr 18388 |
. . . . . 6
⊢ ((𝐾 ∈ Poset ∧ (𝑞 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → ((𝑞(lt‘𝐾)𝑋 ∧ 𝑋 ≤ 𝑃) → 𝑞(lt‘𝐾)𝑃)) |
| 32 | 27, 19, 22, 29, 31 | syl13anc 1374 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → ((𝑞(lt‘𝐾)𝑋 ∧ 𝑋 ≤ 𝑃) → 𝑞(lt‘𝐾)𝑃)) |
| 33 | 25, 32 | mpand 695 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → (𝑋 ≤ 𝑃 → 𝑞(lt‘𝐾)𝑃)) |
| 34 | 17, 33 | mtod 198 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ 𝑞 ∈ 𝐴 ∧ 𝑞( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 ≤ 𝑃) |
| 35 | 34 | rexlimdv3a 3159 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) → (∃𝑞 ∈ 𝐴 𝑞( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ 𝑃)) |
| 36 | 9, 35 | mpd 15 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) → ¬ 𝑋 ≤ 𝑃) |