Step | Hyp | Ref
| Expression |
1 | | cdlemg4.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
2 | | cdlemg4.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | eqid 2738 |
. . . 4
⊢
(join‘𝐾) =
(join‘𝐾) |
4 | | eqid 2738 |
. . . 4
⊢
(meet‘𝐾) =
(meet‘𝐾) |
5 | | cdlemg4.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
6 | | cdlemg4.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
7 | 1, 2, 3, 4, 5, 6 | lhpmcvr2 38038 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) |
8 | 7 | 3adant3 1131 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) |
9 | | simp11 1202 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
10 | | simp2 1136 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑟 ∈ 𝐴) |
11 | | simp3l 1200 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ 𝑟 ≤ 𝑊) |
12 | 10, 11 | jca 512 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊)) |
13 | | simp12 1203 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) |
14 | | simp13 1204 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝐹 ∈ 𝑇) |
15 | | simp3r 1201 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋) |
16 | | cdlemg4.t |
. . . . . . 7
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
17 | 6, 16, 2, 3, 5, 4, 1 | cdlemg2fv 38613 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹‘𝑋) = ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊))) |
18 | 9, 12, 13, 14, 15, 17 | syl122anc 1378 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹‘𝑋) = ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊))) |
19 | | simp11l 1283 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝐾 ∈ HL) |
20 | 19 | hllatd 37378 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝐾 ∈ Lat) |
21 | 2, 5, 6, 16 | ltrnel 38153 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊)) → ((𝐹‘𝑟) ∈ 𝐴 ∧ ¬ (𝐹‘𝑟) ≤ 𝑊)) |
22 | 21 | simpld 495 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊)) → (𝐹‘𝑟) ∈ 𝐴) |
23 | 9, 14, 12, 22 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹‘𝑟) ∈ 𝐴) |
24 | 1, 5 | atbase 37303 |
. . . . . . 7
⊢ ((𝐹‘𝑟) ∈ 𝐴 → (𝐹‘𝑟) ∈ 𝐵) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹‘𝑟) ∈ 𝐵) |
26 | | simp12l 1285 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵) |
27 | | simp11r 1284 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻) |
28 | 1, 6 | lhpbase 38012 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵) |
30 | 1, 4 | latmcl 18158 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑊) ∈ 𝐵) |
31 | 20, 26, 29, 30 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝑋(meet‘𝐾)𝑊) ∈ 𝐵) |
32 | 1, 3 | latjcl 18157 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑟) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑊) ∈ 𝐵) → ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∈ 𝐵) |
33 | 20, 25, 31, 32 | syl3anc 1370 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∈ 𝐵) |
34 | 18, 33 | eqeltrd 2839 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹‘𝑋) ∈ 𝐵) |
35 | 21 | simprd 496 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊)) → ¬ (𝐹‘𝑟) ≤ 𝑊) |
36 | 9, 14, 12, 35 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ (𝐹‘𝑟) ≤ 𝑊) |
37 | 1, 2, 3 | latlej1 18166 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝐹‘𝑟) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑊) ∈ 𝐵) → (𝐹‘𝑟) ≤ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊))) |
38 | 20, 25, 31, 37 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (𝐹‘𝑟) ≤ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊))) |
39 | 1, 2 | lattr 18162 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ ((𝐹‘𝑟) ∈ 𝐵 ∧ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝐹‘𝑟) ≤ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∧ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ≤ 𝑊) → (𝐹‘𝑟) ≤ 𝑊)) |
40 | 20, 25, 33, 29, 39 | syl13anc 1371 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (((𝐹‘𝑟) ≤ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ∧ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ≤ 𝑊) → (𝐹‘𝑟) ≤ 𝑊)) |
41 | 38, 40 | mpand 692 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → (((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ≤ 𝑊 → (𝐹‘𝑟) ≤ 𝑊)) |
42 | 36, 41 | mtod 197 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ≤ 𝑊) |
43 | 18 | breq1d 5084 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ((𝐹‘𝑋) ≤ 𝑊 ↔ ((𝐹‘𝑟)(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) ≤ 𝑊)) |
44 | 42, 43 | mtbird 325 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ¬ (𝐹‘𝑋) ≤ 𝑊) |
45 | 34, 44 | jca 512 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ 𝑟 ∈ 𝐴 ∧ (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋)) → ((𝐹‘𝑋) ∈ 𝐵 ∧ ¬ (𝐹‘𝑋) ≤ 𝑊)) |
46 | 45 | rexlimdv3a 3215 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) → (∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑟(join‘𝐾)(𝑋(meet‘𝐾)𝑊)) = 𝑋) → ((𝐹‘𝑋) ∈ 𝐵 ∧ ¬ (𝐹‘𝑋) ≤ 𝑊))) |
47 | 8, 46 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) → ((𝐹‘𝑋) ∈ 𝐵 ∧ ¬ (𝐹‘𝑋) ≤ 𝑊)) |