Proof of Theorem 2llnjaN
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
⊢
(Base‘𝐾) =
(Base‘𝐾) |
2 | | 2llnja.l |
. 2
⊢ ≤ =
(le‘𝐾) |
3 | | simpl1l 1112 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝐾 ∈ HL) |
4 | | hllat 34650 |
. . 3
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
5 | 3, 4 | syl 17 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝐾 ∈ Lat) |
6 | | simpl21 1139 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑄 ∈ 𝐴) |
7 | | simpl22 1140 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑅 ∈ 𝐴) |
8 | | 2llnja.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
9 | | 2llnja.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
10 | 1, 8, 9 | hlatjcl 34653 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
11 | 3, 6, 7, 10 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
12 | | simpl31 1142 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑆 ∈ 𝐴) |
13 | | simpl32 1143 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑇 ∈ 𝐴) |
14 | 1, 8, 9 | hlatjcl 34653 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
15 | 3, 12, 13, 14 | syl3anc 1326 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) |
16 | 1, 8 | latjcl 17051 |
. . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ∈ (Base‘𝐾)) |
17 | 5, 11, 15, 16 | syl3anc 1326 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ∈ (Base‘𝐾)) |
18 | | simpl1r 1113 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑊 ∈ 𝑃) |
19 | | 2llnja.p |
. . . 4
⊢ 𝑃 = (LPlanes‘𝐾) |
20 | 1, 19 | lplnbase 34820 |
. . 3
⊢ (𝑊 ∈ 𝑃 → 𝑊 ∈ (Base‘𝐾)) |
21 | 18, 20 | syl 17 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑊 ∈ (Base‘𝐾)) |
22 | | simpr1 1067 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑄 ∨ 𝑅) ≤ 𝑊) |
23 | | simpr2 1068 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ∨ 𝑇) ≤ 𝑊) |
24 | 1, 2, 8 | latjle12 17062 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ ((𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊) ↔ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ≤ 𝑊)) |
25 | 5, 11, 15, 21, 24 | syl13anc 1328 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊) ↔ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ≤ 𝑊)) |
26 | 22, 23, 25 | mpbi2and 956 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) ≤ 𝑊) |
27 | 1, 9 | atbase 34576 |
. . . . . . . . . 10
⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾)) |
28 | 13, 27 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑇 ∈ (Base‘𝐾)) |
29 | 1, 8 | latjcl 17051 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ (Base‘𝐾)) |
30 | 5, 11, 28, 29 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ (Base‘𝐾)) |
31 | 1, 9 | atbase 34576 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ 𝐴 → 𝑆 ∈ (Base‘𝐾)) |
32 | 12, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑆 ∈ (Base‘𝐾)) |
33 | 1, 2, 8 | latlej2 17061 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑇 ≤ (𝑆 ∨ 𝑇)) |
34 | 5, 32, 28, 33 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑇 ≤ (𝑆 ∨ 𝑇)) |
35 | 1, 2, 8 | latjlej2 17066 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ (𝑇 ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑇 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))) |
36 | 5, 28, 15, 11, 35 | syl13anc 1328 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑇 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))) |
37 | 34, 36 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))) |
38 | 1, 2, 5, 30, 17, 21, 37, 26 | lattrd 17058 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊) |
39 | 38 | 3adant3 1081 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊) |
40 | | simp11l 1172 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝐾 ∈ HL) |
41 | | simp121 1193 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ∈ 𝐴) |
42 | | simp122 1194 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑅 ∈ 𝐴) |
43 | | simp132 1197 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑇 ∈ 𝐴) |
44 | | simp123 1195 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ≠ 𝑅) |
45 | | simp23 1096 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) |
46 | | simpl3 1066 |
. . . . . . . . . . . . . 14
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → 𝑆 ≤ (𝑄 ∨ 𝑅)) |
47 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → 𝑇 ≤ (𝑄 ∨ 𝑅)) |
48 | 1, 2, 8 | latjle12 17062 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅))) |
49 | 5, 32, 28, 11, 48 | syl13anc 1328 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅))) |
50 | 49 | 3adant3 1081 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅))) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ≤ (𝑄 ∨ 𝑅) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) ↔ (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅))) |
52 | 46, 47, 51 | mpbi2and 956 |
. . . . . . . . . . . . 13
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → (𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅)) |
53 | | simpl3 1066 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) |
54 | 2, 8, 9 | ps-1 34763 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ HL ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅))) |
55 | 3, 53, 6, 7, 54 | syl112anc 1330 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅))) |
56 | 55 | 3adant3 1081 |
. . . . . . . . . . . . . 14
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅))) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → ((𝑆 ∨ 𝑇) ≤ (𝑄 ∨ 𝑅) ↔ (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅))) |
58 | 52, 57 | mpbid 222 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → (𝑆 ∨ 𝑇) = (𝑄 ∨ 𝑅)) |
59 | 58 | eqcomd 2628 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)) → (𝑄 ∨ 𝑅) = (𝑆 ∨ 𝑇)) |
60 | 59 | ex 450 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (𝑇 ≤ (𝑄 ∨ 𝑅) → (𝑄 ∨ 𝑅) = (𝑆 ∨ 𝑇))) |
61 | 60 | necon3ad 2807 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇) → ¬ 𝑇 ≤ (𝑄 ∨ 𝑅))) |
62 | 45, 61 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ¬ 𝑇 ≤ (𝑄 ∨ 𝑅)) |
63 | 2, 8, 9, 19 | lplni2 34823 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ (𝑄 ∨ 𝑅))) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ 𝑃) |
64 | 40, 41, 42, 43, 44, 62, 63 | syl132anc 1344 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ 𝑃) |
65 | | simp11r 1173 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ∈ 𝑃) |
66 | 2, 19 | lplncmp 34848 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ ((𝑄 ∨ 𝑅) ∨ 𝑇) ∈ 𝑃 ∧ 𝑊 ∈ 𝑃) → (((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑇) = 𝑊)) |
67 | 40, 64, 65, 66 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑇) = 𝑊)) |
68 | 39, 67 | mpbid 222 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) = 𝑊) |
69 | 37 | 3adant3 1081 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑇) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))) |
70 | 68, 69 | eqbrtrrd 4677 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))) |
71 | 70 | 3expia 1267 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ≤ (𝑄 ∨ 𝑅) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))) |
72 | 1, 8 | latjcl 17051 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ (Base‘𝐾)) |
73 | 5, 11, 32, 72 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ (Base‘𝐾)) |
74 | 1, 2, 8 | latlej1 17060 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾)) → 𝑆 ≤ (𝑆 ∨ 𝑇)) |
75 | 5, 32, 28, 74 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑆 ≤ (𝑆 ∨ 𝑇)) |
76 | 1, 2, 8 | latjlej2 17066 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ (𝑆 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → (𝑆 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))) |
77 | 5, 32, 15, 11, 76 | syl13anc 1328 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (𝑆 ≤ (𝑆 ∨ 𝑇) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))) |
78 | 75, 77 | mpd 15 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))) |
79 | 1, 2, 5, 73, 17, 21, 78, 26 | lattrd 17058 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊) |
80 | 79 | 3adant3 1081 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊) |
81 | | simp11l 1172 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝐾 ∈ HL) |
82 | | simp121 1193 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ∈ 𝐴) |
83 | | simp122 1194 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑅 ∈ 𝐴) |
84 | | simp131 1196 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑆 ∈ 𝐴) |
85 | | simp123 1195 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑄 ≠ 𝑅) |
86 | | simp3 1063 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) |
87 | 2, 8, 9, 19 | lplni2 34823 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅))) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑃) |
88 | 81, 82, 83, 84, 85, 86, 87 | syl132anc 1344 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑃) |
89 | | simp11r 1173 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ∈ 𝑃) |
90 | 2, 19 | lplncmp 34848 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ ((𝑄 ∨ 𝑅) ∨ 𝑆) ∈ 𝑃 ∧ 𝑊 ∈ 𝑃) → (((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑆) = 𝑊)) |
91 | 81, 88, 89, 90 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → (((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ 𝑊 ↔ ((𝑄 ∨ 𝑅) ∨ 𝑆) = 𝑊)) |
92 | 80, 91 | mpbid 222 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) = 𝑊) |
93 | 78 | 3adant3 1081 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → ((𝑄 ∨ 𝑅) ∨ 𝑆) ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))) |
94 | 92, 93 | eqbrtrrd 4677 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇)) ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅)) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))) |
95 | 94 | 3expia 1267 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → (¬ 𝑆 ≤ (𝑄 ∨ 𝑅) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)))) |
96 | 71, 95 | pm2.61d 170 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → 𝑊 ≤ ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇))) |
97 | 1, 2, 5, 17, 21, 26, 96 | latasymd 17057 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) = 𝑊) |