Step | Hyp | Ref
| Expression |
1 | | 3dim0.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
2 | | 3dim0.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | 3dim0.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
4 | 1, 2, 3 | 3dim2 34754 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → ∃𝑣 ∈ 𝐴 ∃𝑤 ∈ 𝐴 (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) |
5 | 4 | 3adant3r1 1274 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ∃𝑣 ∈ 𝐴 ∃𝑤 ∈ 𝐴 (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) |
6 | | simpl2l 1114 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 = 𝑄) → 𝑣 ∈ 𝐴) |
7 | | simp3l 1089 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → ¬ 𝑣 ≤ (𝑄 ∨ 𝑅)) |
8 | | simp1l 1085 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → 𝐾 ∈ HL) |
9 | | simp1r2 1158 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → 𝑄 ∈ 𝐴) |
10 | 1, 3 | hlatjidm 34655 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑄 ∨ 𝑄) = 𝑄) |
11 | 8, 9, 10 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → (𝑄 ∨ 𝑄) = 𝑄) |
12 | 11 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → ((𝑄 ∨ 𝑄) ∨ 𝑅) = (𝑄 ∨ 𝑅)) |
13 | 12 | breq2d 4665 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → (𝑣 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅) ↔ 𝑣 ≤ (𝑄 ∨ 𝑅))) |
14 | 7, 13 | mtbird 315 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → ¬ 𝑣 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)) |
15 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑃 = 𝑄 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑄)) |
16 | 15 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑃 = 𝑄 → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑄 ∨ 𝑄) ∨ 𝑅)) |
17 | 16 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑃 = 𝑄 → (𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑣 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅))) |
18 | 17 | notbid 308 |
. . . . . . . 8
⊢ (𝑃 = 𝑄 → (¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ¬ 𝑣 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅))) |
19 | 18 | biimparc 504 |
. . . . . . 7
⊢ ((¬
𝑣 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅) ∧ 𝑃 = 𝑄) → ¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
20 | 14, 19 | sylan 488 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 = 𝑄) → ¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
21 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑠 = 𝑣 → (𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
22 | 21 | notbid 308 |
. . . . . . 7
⊢ (𝑠 = 𝑣 → (¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
23 | 22 | rspcev 3309 |
. . . . . 6
⊢ ((𝑣 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
24 | 6, 20, 23 | syl2anc 693 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 = 𝑄) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
25 | | simp2l 1087 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → 𝑣 ∈ 𝐴) |
26 | 25 | ad2antrr 762 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → 𝑣 ∈ 𝐴) |
27 | 7 | ad2antrr 762 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → ¬ 𝑣 ≤ (𝑄 ∨ 𝑅)) |
28 | 1, 3 | hlatjass 34656 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ (𝑄 ∨ 𝑅))) |
29 | 28 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ (𝑄 ∨ 𝑅))) |
30 | 29 | ad2antrr 762 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ (𝑄 ∨ 𝑅))) |
31 | | hllat 34650 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
32 | 8, 31 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → 𝐾 ∈ Lat) |
33 | | simp1r1 1157 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → 𝑃 ∈ 𝐴) |
34 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐾) =
(Base‘𝐾) |
35 | 34, 3 | atbase 34576 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → 𝑃 ∈ (Base‘𝐾)) |
37 | | simp1r3 1159 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → 𝑅 ∈ 𝐴) |
38 | 34, 1, 3 | hlatjcl 34653 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
39 | 8, 9, 37, 38 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
40 | 32, 36, 39 | 3jca 1242 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → (𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) |
41 | 40 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) → (𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) |
42 | 34, 2, 1 | latleeqj1 17063 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ (𝑄 ∨ 𝑅)) = (𝑄 ∨ 𝑅))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ (𝑄 ∨ 𝑅)) = (𝑄 ∨ 𝑅))) |
44 | 43 | biimpa 501 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → (𝑃 ∨ (𝑄 ∨ 𝑅)) = (𝑄 ∨ 𝑅)) |
45 | 30, 44 | eqtrd 2656 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑄 ∨ 𝑅)) |
46 | 45 | breq2d 4665 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → (𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑣 ≤ (𝑄 ∨ 𝑅))) |
47 | 27, 46 | mtbird 315 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → ¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
48 | 26, 47, 23 | syl2anc 693 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
49 | | simpl2r 1115 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) → 𝑤 ∈ 𝐴) |
50 | 49 | ad2antrr 762 |
. . . . . . . 8
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → 𝑤 ∈ 𝐴) |
51 | 8, 33, 9 | 3jca 1242 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) |
52 | 51 | ad3antrrr 766 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) |
53 | 37, 25 | jca 554 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → (𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) |
54 | 53 | ad3antrrr 766 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → (𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) |
55 | | simpl3r 1117 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) → ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) |
56 | 55 | ad2antrr 762 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) |
57 | | simplr 792 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) |
58 | | simpr 477 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) |
59 | 1, 2, 3 | 3dimlem3a 34746 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → ¬ 𝑤 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
60 | 52, 54, 56, 57, 58, 59 | syl113anc 1338 |
. . . . . . . 8
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ¬ 𝑤 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
61 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑤 → (𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑤 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
62 | 61 | notbid 308 |
. . . . . . . . 9
⊢ (𝑠 = 𝑤 → (¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ¬ 𝑤 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
63 | 62 | rspcev 3309 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐴 ∧ ¬ 𝑤 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
64 | 50, 60, 63 | syl2anc 693 |
. . . . . . 7
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
65 | | simpl2l 1114 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) → 𝑣 ∈ 𝐴) |
66 | 65 | ad2antrr 762 |
. . . . . . . 8
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → 𝑣 ∈ 𝐴) |
67 | 51 | ad3antrrr 766 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → (𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) |
68 | 53 | ad3antrrr 766 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → (𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴)) |
69 | | simpl3l 1116 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) → ¬ 𝑣 ≤ (𝑄 ∨ 𝑅)) |
70 | 69 | ad2antrr 762 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ¬ 𝑣 ≤ (𝑄 ∨ 𝑅)) |
71 | | simplr 792 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) |
72 | | simpr 477 |
. . . . . . . . 9
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) |
73 | 1, 2, 3 | 3dimlem4a 34749 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → ¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
74 | 67, 68, 70, 71, 72, 73 | syl113anc 1338 |
. . . . . . . 8
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ¬ 𝑣 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
75 | 66, 74, 23 | syl2anc 693 |
. . . . . . 7
⊢
((((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
76 | 64, 75 | pm2.61dan 832 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
77 | 48, 76 | pm2.61dan 832 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) ∧ 𝑃 ≠ 𝑄) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
78 | 24, 77 | pm2.61dane 2881 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣))) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |
79 | 78 | 3exp 1264 |
. . 3
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))) |
80 | 79 | rexlimdvv 3037 |
. 2
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (∃𝑣 ∈ 𝐴 ∃𝑤 ∈ 𝐴 (¬ 𝑣 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑤 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑣)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) |
81 | 5, 80 | mpd 15 |
1
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) |