Proof of Theorem cdlemg27b
Step | Hyp | Ref
| Expression |
1 | | simp11 1091 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | simp12 1092 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
3 | | simp13 1093 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
4 | | simp22 1095 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊)) |
5 | | simp23l 1182 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝐹 ∈ 𝑇) |
6 | | simp31 1097 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑣 ≠ (𝑅‘𝐹)) |
7 | | cdlemg12.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
8 | | cdlemg12.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
9 | | cdlemg12.m |
. . . . . 6
⊢ ∧ =
(meet‘𝐾) |
10 | | cdlemg12.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
11 | | cdlemg12.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
12 | | cdlemg12.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
13 | | cdlemg12b.r |
. . . . . 6
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
14 | | cdlemg31.n |
. . . . . 6
⊢ 𝑁 = ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))) |
15 | 7, 8, 9, 10, 11, 12, 13, 14 | cdlemg31b0a 35983 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝑣 ≠ (𝑅‘𝐹))) → (𝑁 ∈ 𝐴 ∨ 𝑁 = (0.‘𝐾))) |
16 | 1, 2, 3, 4, 5, 6, 15 | syl132anc 1344 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑁 ∈ 𝐴 ∨ 𝑁 = (0.‘𝐾))) |
17 | | simp23r 1183 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑧 ≠ 𝑁) |
18 | 17 | adantr 481 |
. . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 = (0.‘𝐾))) → 𝑧 ≠ 𝑁) |
19 | | simp11l 1172 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝐾 ∈ HL) |
20 | 19 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 ∈ 𝐴) → 𝐾 ∈ HL) |
21 | | hlatl 34647 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
22 | 20, 21 | syl 17 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 ∈ 𝐴) → 𝐾 ∈ AtLat) |
23 | | simpl21 1139 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
24 | | simpr 477 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 ∈ 𝐴) → 𝑁 ∈ 𝐴) |
25 | 7, 10 | atcmp 34598 |
. . . . . . . 8
⊢ ((𝐾 ∈ AtLat ∧ 𝑧 ∈ 𝐴 ∧ 𝑁 ∈ 𝐴) → (𝑧 ≤ 𝑁 ↔ 𝑧 = 𝑁)) |
26 | 22, 23, 24, 25 | syl3anc 1326 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 ∈ 𝐴) → (𝑧 ≤ 𝑁 ↔ 𝑧 = 𝑁)) |
27 | 26 | necon3bbid 2831 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 ∈ 𝐴) → (¬ 𝑧 ≤ 𝑁 ↔ 𝑧 ≠ 𝑁)) |
28 | 19 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝐾 ∈ HL) |
29 | 28, 21 | syl 17 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝐾 ∈ AtLat) |
30 | | simpl21 1139 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝑧 ∈ 𝐴) |
31 | | eqid 2622 |
. . . . . . . . . 10
⊢
(0.‘𝐾) =
(0.‘𝐾) |
32 | 7, 31, 10 | atnle0 34596 |
. . . . . . . . 9
⊢ ((𝐾 ∈ AtLat ∧ 𝑧 ∈ 𝐴) → ¬ 𝑧 ≤ (0.‘𝐾)) |
33 | 29, 30, 32 | syl2anc 693 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → ¬ 𝑧 ≤ (0.‘𝐾)) |
34 | | simpr 477 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝑁 = (0.‘𝐾)) |
35 | 34 | breq2d 4665 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → (𝑧 ≤ 𝑁 ↔ 𝑧 ≤ (0.‘𝐾))) |
36 | 33, 35 | mtbird 315 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → ¬ 𝑧 ≤ 𝑁) |
37 | 17 | adantr 481 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → 𝑧 ≠ 𝑁) |
38 | 36, 37 | 2thd 255 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ 𝑁 = (0.‘𝐾)) → (¬ 𝑧 ≤ 𝑁 ↔ 𝑧 ≠ 𝑁)) |
39 | 27, 38 | jaodan 826 |
. . . . 5
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 = (0.‘𝐾))) → (¬ 𝑧 ≤ 𝑁 ↔ 𝑧 ≠ 𝑁)) |
40 | 18, 39 | mpbird 247 |
. . . 4
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 = (0.‘𝐾))) → ¬ 𝑧 ≤ 𝑁) |
41 | 16, 40 | mpdan 702 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ¬ 𝑧 ≤ 𝑁) |
42 | | simp32 1098 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑧 ≤ (𝑃 ∨ 𝑣)) |
43 | | hllat 34650 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
44 | 19, 43 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝐾 ∈ Lat) |
45 | | simp21 1094 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑧 ∈ 𝐴) |
46 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝐾) =
(Base‘𝐾) |
47 | 46, 10 | atbase 34576 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (Base‘𝐾)) |
48 | 45, 47 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑧 ∈ (Base‘𝐾)) |
49 | | simp12l 1174 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑃 ∈ 𝐴) |
50 | | simp22l 1180 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑣 ∈ 𝐴) |
51 | 46, 8, 10 | hlatjcl 34653 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑃 ∨ 𝑣) ∈ (Base‘𝐾)) |
52 | 19, 49, 50, 51 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑃 ∨ 𝑣) ∈ (Base‘𝐾)) |
53 | | simp13l 1176 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → 𝑄 ∈ 𝐴) |
54 | | simp33 1099 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝐹‘𝑃) ≠ 𝑃) |
55 | 7, 10, 11, 12, 13 | trlat 35456 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ∈ 𝐴) |
56 | 1, 2, 5, 54, 55 | syl112anc 1330 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ∈ 𝐴) |
57 | 46, 8, 10 | hlatjcl 34653 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ (𝑅‘𝐹) ∈ 𝐴) → (𝑄 ∨ (𝑅‘𝐹)) ∈ (Base‘𝐾)) |
58 | 19, 53, 56, 57 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑄 ∨ (𝑅‘𝐹)) ∈ (Base‘𝐾)) |
59 | 46, 7, 9 | latlem12 17078 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑧 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑣) ∈ (Base‘𝐾) ∧ (𝑄 ∨ (𝑅‘𝐹)) ∈ (Base‘𝐾))) → ((𝑧 ≤ (𝑃 ∨ 𝑣) ∧ 𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹))) ↔ 𝑧 ≤ ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))))) |
60 | 44, 48, 52, 58, 59 | syl13anc 1328 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ((𝑧 ≤ (𝑃 ∨ 𝑣) ∧ 𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹))) ↔ 𝑧 ≤ ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹))))) |
61 | 14 | breq2i 4661 |
. . . . . 6
⊢ (𝑧 ≤ 𝑁 ↔ 𝑧 ≤ ((𝑃 ∨ 𝑣) ∧ (𝑄 ∨ (𝑅‘𝐹)))) |
62 | 60, 61 | syl6bbr 278 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ((𝑧 ≤ (𝑃 ∨ 𝑣) ∧ 𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹))) ↔ 𝑧 ≤ 𝑁)) |
63 | 62 | biimpd 219 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ((𝑧 ≤ (𝑃 ∨ 𝑣) ∧ 𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹))) → 𝑧 ≤ 𝑁)) |
64 | 42, 63 | mpand 711 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹)) → 𝑧 ≤ 𝑁)) |
65 | 41, 64 | mtod 189 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ¬ 𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹))) |
66 | 7, 11, 12, 13 | trlle 35471 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ≤ 𝑊) |
67 | 1, 5, 66 | syl2anc 693 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ≤ 𝑊) |
68 | | simp13r 1177 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ¬ 𝑄 ≤ 𝑊) |
69 | | nbrne2 4673 |
. . . 4
⊢ (((𝑅‘𝐹) ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊) → (𝑅‘𝐹) ≠ 𝑄) |
70 | 67, 68, 69 | syl2anc 693 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ≠ 𝑄) |
71 | 7, 8, 10 | hlatexch1 34681 |
. . 3
⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝐹) ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅‘𝐹) ≠ 𝑄) → ((𝑅‘𝐹) ≤ (𝑄 ∨ 𝑧) → 𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹)))) |
72 | 19, 56, 45, 53, 70, 71 | syl131anc 1339 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ((𝑅‘𝐹) ≤ (𝑄 ∨ 𝑧) → 𝑧 ≤ (𝑄 ∨ (𝑅‘𝐹)))) |
73 | 65, 72 | mtod 189 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑧 ∈ 𝐴 ∧ (𝑣 ∈ 𝐴 ∧ 𝑣 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ 𝑧 ≠ 𝑁)) ∧ (𝑣 ≠ (𝑅‘𝐹) ∧ 𝑧 ≤ (𝑃 ∨ 𝑣) ∧ (𝐹‘𝑃) ≠ 𝑃)) → ¬ (𝑅‘𝐹) ≤ (𝑄 ∨ 𝑧)) |