Proof of Theorem cdleme19d
Step | Hyp | Ref
| Expression |
1 | | cdleme19.l |
. . 3
⊢ ≤ =
(le‘𝐾) |
2 | | cdleme19.j |
. . 3
⊢ ∨ =
(join‘𝐾) |
3 | | cdleme19.m |
. . 3
⊢ ∧ =
(meet‘𝐾) |
4 | | cdleme19.a |
. . 3
⊢ 𝐴 = (Atoms‘𝐾) |
5 | | cdleme19.h |
. . 3
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | cdleme19.u |
. . 3
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
7 | | cdleme19.f |
. . 3
⊢ 𝐹 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊))) |
8 | | cdleme19.g |
. . 3
⊢ 𝐺 = ((𝑇 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑇) ∧ 𝑊))) |
9 | | cdleme19.d |
. . 3
⊢ 𝐷 = ((𝑅 ∨ 𝑆) ∧ 𝑊) |
10 | | cdleme19.y |
. . 3
⊢ 𝑌 = ((𝑅 ∨ 𝑇) ∧ 𝑊) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cdleme19b 38318 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐷 ≤ (𝐹 ∨ 𝐺)) |
12 | | simp11l 1283 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐾 ∈ HL) |
13 | | hlcvl 37373 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) |
14 | 12, 13 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐾 ∈ CvLat) |
15 | | simp11r 1284 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝑊 ∈ 𝐻) |
16 | | simp21l 1289 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝑆 ∈ 𝐴) |
17 | | simp21r 1290 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑆 ≤ 𝑊) |
18 | | simp23 1207 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝑅 ∈ 𝐴) |
19 | | simp33l 1299 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝑅 ≤ (𝑃 ∨ 𝑄)) |
20 | | simp32l 1297 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)) |
21 | 1, 2, 3, 4, 5, 9 | cdlemeda 38312 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝐷 ∈ 𝐴) |
22 | 12, 15, 16, 17, 18, 19, 20, 21 | syl223anc 1395 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐷 ∈ 𝐴) |
23 | | simp11 1202 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
24 | | simp12 1203 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
25 | | simp13 1204 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
26 | | simp22 1206 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) |
27 | | simp31l 1295 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝑃 ≠ 𝑄) |
28 | | simp32r 1298 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) |
29 | 1, 2, 3, 4, 5, 6, 8 | cdleme3fa 38250 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄))) → 𝐺 ∈ 𝐴) |
30 | 23, 24, 25, 26, 27, 28, 29 | syl132anc 1387 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐺 ∈ 𝐴) |
31 | | simp21 1205 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) |
32 | 1, 2, 3, 4, 5, 6, 7 | cdleme3fa 38250 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝐹 ∈ 𝐴) |
33 | 23, 24, 25, 31, 27, 20, 32 | syl132anc 1387 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐹 ∈ 𝐴) |
34 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cdleme19c 38319 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝐹 ≠ 𝐷) |
35 | 12, 15, 24, 25, 31, 18, 27, 20, 34 | syl233anc 1398 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐹 ≠ 𝐷) |
36 | 35 | necomd 2999 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → 𝐷 ≠ 𝐹) |
37 | 1, 2, 4 | cvlatexchb1 37348 |
. . 3
⊢ ((𝐾 ∈ CvLat ∧ (𝐷 ∈ 𝐴 ∧ 𝐺 ∈ 𝐴 ∧ 𝐹 ∈ 𝐴) ∧ 𝐷 ≠ 𝐹) → (𝐷 ≤ (𝐹 ∨ 𝐺) ↔ (𝐹 ∨ 𝐷) = (𝐹 ∨ 𝐺))) |
38 | 14, 22, 30, 33, 36, 37 | syl131anc 1382 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → (𝐷 ≤ (𝐹 ∨ 𝐺) ↔ (𝐹 ∨ 𝐷) = (𝐹 ∨ 𝐺))) |
39 | 11, 38 | mpbid 231 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇) ∧ (¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑅 ≤ (𝑆 ∨ 𝑇)))) → (𝐹 ∨ 𝐷) = (𝐹 ∨ 𝐺)) |