Proof of Theorem paddasslem2
Step | Hyp | Ref
| Expression |
1 | | simp1l 1199 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝐾 ∈ HL) |
2 | | simp1r 1200 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑟 ∈ 𝐴) |
3 | | simp23 1210 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑧 ∈ 𝐴) |
4 | | simp22 1209 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑦 ∈ 𝐴) |
5 | 2, 3, 4 | 3jca 1130 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → (𝑟 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) |
6 | | simp21 1208 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑥 ∈ 𝐴) |
7 | | simp3l 1203 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → ¬ 𝑟 ≤ (𝑥 ∨ 𝑦)) |
8 | | paddasslem.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
9 | | paddasslem.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
10 | | paddasslem.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
11 | 8, 9, 10 | atnlej2 37168 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑟 ≤ (𝑥 ∨ 𝑦)) → 𝑟 ≠ 𝑦) |
12 | 1, 2, 6, 4, 7, 11 | syl131anc 1385 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑟 ≠ 𝑦) |
13 | 1, 5, 12 | 3jca 1130 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → (𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑟 ≠ 𝑦)) |
14 | | simp3r 1204 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑟 ≤ (𝑦 ∨ 𝑧)) |
15 | 8, 9, 10 | hlatexch1 37183 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑟 ≠ 𝑦) → (𝑟 ≤ (𝑦 ∨ 𝑧) → 𝑧 ≤ (𝑦 ∨ 𝑟))) |
16 | 13, 14, 15 | sylc 65 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑧 ≤ (𝑦 ∨ 𝑟)) |
17 | 1 | hllatd 37152 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝐾 ∈ Lat) |
18 | | eqid 2739 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
19 | 18, 10 | atbase 37077 |
. . . 4
⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ (Base‘𝐾)) |
20 | 2, 19 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑟 ∈ (Base‘𝐾)) |
21 | 18, 10 | atbase 37077 |
. . . 4
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ (Base‘𝐾)) |
22 | 4, 21 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑦 ∈ (Base‘𝐾)) |
23 | 18, 9 | latjcom 17986 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ 𝑟 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝑟 ∨ 𝑦) = (𝑦 ∨ 𝑟)) |
24 | 17, 20, 22, 23 | syl3anc 1373 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → (𝑟 ∨ 𝑦) = (𝑦 ∨ 𝑟)) |
25 | 16, 24 | breqtrrd 5098 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑧 ≤ (𝑟 ∨ 𝑦)) |