Step | Hyp | Ref
| Expression |
1 | | simp11 1201 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → 𝐾 ∈ HL) |
2 | | simp12 1202 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → 𝑃 ∈ 𝐴) |
3 | | simp13 1203 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → 𝑄 ∈ 𝐴) |
4 | | simp21 1204 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → 𝑅 ∈ 𝐴) |
5 | 2, 3, 4 | 3jca 1126 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) |
6 | | simp22 1205 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → 𝑆 ∈ 𝐴) |
7 | | simp23 1206 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → 𝑇 ∈ 𝐴) |
8 | 6, 7 | jca 511 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) |
9 | | simp31 1207 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) |
10 | | simp32 1208 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → 𝑆 ≠ 𝑇) |
11 | 9, 10 | jca 511 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇)) |
12 | | simp33 1209 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅))) |
13 | | ps-2b.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
14 | | ps-2b.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
15 | | ps-2b.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
16 | 13, 14, 15 | ps-2 37471 |
. . 3
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇) ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → ∃𝑢 ∈ 𝐴 (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) |
17 | 1, 5, 8, 11, 12, 16 | syl32anc 1376 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → ∃𝑢 ∈ 𝐴 (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) |
18 | | simp111 1300 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ HL) |
19 | | hlatl 37353 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ AtLat) |
21 | 18 | hllatd 37357 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝐾 ∈ Lat) |
22 | | simp112 1301 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝑃 ∈ 𝐴) |
23 | | simp121 1303 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝑅 ∈ 𝐴) |
24 | | eqid 2739 |
. . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) |
25 | 24, 14, 15 | hlatjcl 37360 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾)) |
26 | 18, 22, 23, 25 | syl3anc 1369 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾)) |
27 | | simp122 1304 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝑆 ∈ 𝐴) |
28 | | simp123 1305 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝑇 ∈ 𝐴) |
29 | 24, 14, 15 | hlatjcl 37360 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
30 | 18, 27, 28, 29 | syl3anc 1369 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
31 | | ps-2b.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
32 | 24, 31 | latmcl 18139 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ∈ (Base‘𝐾)) |
33 | 21, 26, 30, 32 | syl3anc 1369 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ∈ (Base‘𝐾)) |
34 | | simp2 1135 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝑢 ∈ 𝐴) |
35 | | simp3 1136 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) |
36 | 24, 15 | atbase 37282 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐴 → 𝑢 ∈ (Base‘𝐾)) |
37 | 34, 36 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝑢 ∈ (Base‘𝐾)) |
38 | 24, 13, 31 | latlem12 18165 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝑢 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾))) → ((𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇)) ↔ 𝑢 ≤ ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)))) |
39 | 21, 37, 26, 30, 38 | syl13anc 1370 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → ((𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇)) ↔ 𝑢 ≤ ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)))) |
40 | 35, 39 | mpbid 231 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → 𝑢 ≤ ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇))) |
41 | | ps-2b.z |
. . . . 5
⊢ 0 =
(0.‘𝐾) |
42 | 24, 13, 41, 15 | atlen0 37303 |
. . . 4
⊢ (((𝐾 ∈ AtLat ∧ ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ∈ (Base‘𝐾) ∧ 𝑢 ∈ 𝐴) ∧ 𝑢 ≤ ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇))) → ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ≠ 0 ) |
43 | 20, 33, 34, 40, 42 | syl31anc 1371 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) ∧ 𝑢 ∈ 𝐴 ∧ (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) → ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ≠ 0 ) |
44 | 43 | rexlimdv3a 3216 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → (∃𝑢 ∈ 𝐴 (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇)) → ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ≠ 0 )) |
45 | 17, 44 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ≠ 0 ) |