Proof of Theorem cdlemg18b
Step | Hyp | Ref
| Expression |
1 | | simp33 1210 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄))) → ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) |
2 | | simp3r 1201 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄))) |
3 | | simp1l 1196 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝐾 ∈ HL) |
4 | | simp1r 1197 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑊 ∈ 𝐻) |
5 | | simp21 1205 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
6 | | simp22l 1291 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑄 ∈ 𝐴) |
7 | | simp3l1 1277 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑃 ≠ 𝑄) |
8 | | cdlemg12.l |
. . . . . . . . . . . . 13
⊢ ≤ =
(le‘𝐾) |
9 | | cdlemg12.j |
. . . . . . . . . . . . 13
⊢ ∨ =
(join‘𝐾) |
10 | | cdlemg12.m |
. . . . . . . . . . . . 13
⊢ ∧ =
(meet‘𝐾) |
11 | | cdlemg12.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = (Atoms‘𝐾) |
12 | | cdlemg12.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (LHyp‘𝐾) |
13 | | cdlemg18b.u |
. . . . . . . . . . . . 13
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
14 | 8, 9, 10, 11, 12, 13 | cdleme0a 38221 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑈 ∈ 𝐴) |
15 | 3, 4, 5, 6, 7, 14 | syl212anc 1379 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑈 ∈ 𝐴) |
16 | | simp1 1135 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
17 | | simp23 1207 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝐹 ∈ 𝑇) |
18 | | cdlemg12.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
19 | 8, 11, 12, 18 | ltrnat 38150 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐴) → (𝐹‘𝑄) ∈ 𝐴) |
20 | 16, 17, 6, 19 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝐹‘𝑄) ∈ 𝐴) |
21 | 8, 9, 11 | hlatlej1 37385 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ (𝐹‘𝑄) ∈ 𝐴) → 𝑈 ≤ (𝑈 ∨ (𝐹‘𝑄))) |
22 | 3, 15, 20, 21 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑈 ≤ (𝑈 ∨ (𝐹‘𝑄))) |
23 | 3 | hllatd 37374 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝐾 ∈ Lat) |
24 | | simp21l 1289 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑃 ∈ 𝐴) |
25 | | eqid 2740 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐾) =
(Base‘𝐾) |
26 | 25, 11 | atbase 37299 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
27 | 24, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑃 ∈ (Base‘𝐾)) |
28 | 25, 11 | atbase 37299 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾)) |
29 | 15, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → 𝑈 ∈ (Base‘𝐾)) |
30 | 25, 9, 11 | hlatjcl 37377 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ (𝐹‘𝑄) ∈ 𝐴) → (𝑈 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾)) |
31 | 3, 15, 20, 30 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑈 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾)) |
32 | 25, 8, 9 | latjle12 18166 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑈 ∨ (𝐹‘𝑄)) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)) ∧ 𝑈 ≤ (𝑈 ∨ (𝐹‘𝑄))) ↔ (𝑃 ∨ 𝑈) ≤ (𝑈 ∨ (𝐹‘𝑄)))) |
33 | 23, 27, 29, 31, 32 | syl13anc 1371 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → ((𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)) ∧ 𝑈 ≤ (𝑈 ∨ (𝐹‘𝑄))) ↔ (𝑃 ∨ 𝑈) ≤ (𝑈 ∨ (𝐹‘𝑄)))) |
34 | 2, 22, 33 | mpbi2and 709 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑃 ∨ 𝑈) ≤ (𝑈 ∨ (𝐹‘𝑄))) |
35 | 8, 9, 10, 11, 12, 13 | cdleme0cp 38224 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴)) → (𝑃 ∨ 𝑈) = (𝑃 ∨ 𝑄)) |
36 | 3, 4, 5, 6, 35 | syl22anc 836 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑃 ∨ 𝑈) = (𝑃 ∨ 𝑄)) |
37 | | simp22 1206 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
38 | 12, 18, 8, 9, 11, 10, 13 | cdlemg2kq 38612 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝐹 ∈ 𝑇) → ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) = ((𝐹‘𝑄) ∨ 𝑈)) |
39 | 16, 5, 37, 17, 38 | syl121anc 1374 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) = ((𝐹‘𝑄) ∨ 𝑈)) |
40 | 9, 11 | hlatjcom 37378 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑄) ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → ((𝐹‘𝑄) ∨ 𝑈) = (𝑈 ∨ (𝐹‘𝑄))) |
41 | 3, 20, 15, 40 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → ((𝐹‘𝑄) ∨ 𝑈) = (𝑈 ∨ (𝐹‘𝑄))) |
42 | 39, 41 | eqtr2d 2781 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑈 ∨ (𝐹‘𝑄)) = ((𝐹‘𝑃) ∨ (𝐹‘𝑄))) |
43 | 34, 36, 42 | 3brtr3d 5110 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑃 ∨ 𝑄) ≤ ((𝐹‘𝑃) ∨ (𝐹‘𝑄))) |
44 | 8, 11, 12, 18 | ltrnat 38150 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐹‘𝑃) ∈ 𝐴) |
45 | 16, 17, 24, 44 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝐹‘𝑃) ∈ 𝐴) |
46 | 8, 9, 11 | ps-1 37487 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ (𝐹‘𝑄) ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) ↔ (𝑃 ∨ 𝑄) = ((𝐹‘𝑃) ∨ (𝐹‘𝑄)))) |
47 | 3, 24, 6, 7, 45, 20, 46 | syl132anc 1387 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → ((𝑃 ∨ 𝑄) ≤ ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) ↔ (𝑃 ∨ 𝑄) = ((𝐹‘𝑃) ∨ (𝐹‘𝑄)))) |
48 | 43, 47 | mpbid 231 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → (𝑃 ∨ 𝑄) = ((𝐹‘𝑃) ∨ (𝐹‘𝑄))) |
49 | 9, 11 | hlatjcom 37378 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ (𝐹‘𝑄) ∈ 𝐴) → ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) = ((𝐹‘𝑄) ∨ (𝐹‘𝑃))) |
50 | 3, 45, 20, 49 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → ((𝐹‘𝑃) ∨ (𝐹‘𝑄)) = ((𝐹‘𝑄) ∨ (𝐹‘𝑃))) |
51 | 48, 50 | eqtr2d 2781 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) → ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) = (𝑃 ∨ 𝑄)) |
52 | 51 | 3exp 1118 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) → (((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) ∧ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄))) → ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) = (𝑃 ∨ 𝑄)))) |
53 | 52 | exp4a 432 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) → ((𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄)) → (𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)) → ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) = (𝑃 ∨ 𝑄))))) |
54 | 53 | 3imp 1110 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄))) → (𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)) → ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) = (𝑃 ∨ 𝑄))) |
55 | 54 | necon3ad 2958 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄))) → (((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄) → ¬ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄)))) |
56 | 1, 55 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ≠ 𝑄 ∧ (𝐹‘𝑃) ≠ 𝑄 ∧ ((𝐹‘𝑄) ∨ (𝐹‘𝑃)) ≠ (𝑃 ∨ 𝑄))) → ¬ 𝑃 ≤ (𝑈 ∨ (𝐹‘𝑄))) |