Step | Hyp | Ref
| Expression |
1 | | simp3 1137 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → 𝑌 ∈ 𝑁) |
2 | | eqid 2740 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
3 | | eqid 2740 |
. . . . 5
⊢
(join‘𝐾) =
(join‘𝐾) |
4 | | eqid 2740 |
. . . . 5
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
5 | | lplnnlelln.n |
. . . . 5
⊢ 𝑁 = (LLines‘𝐾) |
6 | 2, 3, 4, 5 | islln2 37521 |
. . . 4
⊢ (𝐾 ∈ HL → (𝑌 ∈ 𝑁 ↔ (𝑌 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))))) |
7 | 6 | 3ad2ant1 1132 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → (𝑌 ∈ 𝑁 ↔ (𝑌 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))))) |
8 | 1, 7 | mpbid 231 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → (𝑌 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟)))) |
9 | | simp11 1202 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → 𝐾 ∈ HL) |
10 | | simp12 1203 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → 𝑋 ∈ 𝑃) |
11 | | simp2l 1198 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → 𝑞 ∈ (Atoms‘𝐾)) |
12 | | simp2r 1199 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → 𝑟 ∈ (Atoms‘𝐾)) |
13 | | lplnnlelln.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
14 | | lplnnlelln.p |
. . . . . . . 8
⊢ 𝑃 = (LPlanes‘𝐾) |
15 | 13, 3, 4, 14 | lplnnle2at 37551 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑃 ∧ 𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾))) → ¬ 𝑋 ≤ (𝑞(join‘𝐾)𝑟)) |
16 | 9, 10, 11, 12, 15 | syl13anc 1371 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → ¬ 𝑋 ≤ (𝑞(join‘𝐾)𝑟)) |
17 | | simp3r 1201 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → 𝑌 = (𝑞(join‘𝐾)𝑟)) |
18 | 17 | breq2d 5091 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → (𝑋 ≤ 𝑌 ↔ 𝑋 ≤ (𝑞(join‘𝐾)𝑟))) |
19 | 16, 18 | mtbird 325 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) ∧ (𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → ¬ 𝑋 ≤ 𝑌) |
20 | 19 | 3exp 1118 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → ((𝑞 ∈ (Atoms‘𝐾) ∧ 𝑟 ∈ (Atoms‘𝐾)) → ((𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟)) → ¬ 𝑋 ≤ 𝑌))) |
21 | 20 | rexlimdvv 3224 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → (∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟)) → ¬ 𝑋 ≤ 𝑌)) |
22 | 21 | adantld 491 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → ((𝑌 ∈ (Base‘𝐾) ∧ ∃𝑞 ∈ (Atoms‘𝐾)∃𝑟 ∈ (Atoms‘𝐾)(𝑞 ≠ 𝑟 ∧ 𝑌 = (𝑞(join‘𝐾)𝑟))) → ¬ 𝑋 ≤ 𝑌)) |
23 | 8, 22 | mpd 15 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) → ¬ 𝑋 ≤ 𝑌) |