Step | Hyp | Ref
| Expression |
1 | | dihglblem.b |
. 2
⊢ 𝐵 = (Base‘𝐾) |
2 | | dihglblem.l |
. 2
⊢ ≤ =
(le‘𝐾) |
3 | | dihglblem.g |
. 2
⊢ 𝐺 = (glb‘𝐾) |
4 | | simpl1l 1105 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL) |
5 | | hllat 33668 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ Lat) |
7 | | simp1l 1078 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ HL) |
8 | | hlclat 33663 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝐾 ∈ CLat) |
10 | | dihglblem.t |
. . . . . 6
⊢ 𝑇 = {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} |
11 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} ⊆ 𝐵 |
12 | 10, 11 | eqsstri 3598 |
. . . . 5
⊢ 𝑇 ⊆ 𝐵 |
13 | 1, 3 | clatglbcl 16937 |
. . . . 5
⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵) → (𝐺‘𝑇) ∈ 𝐵) |
14 | 9, 12, 13 | sylancl 693 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑇) ∈ 𝐵) |
15 | 14 | adantr 480 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑇) ∈ 𝐵) |
16 | | simpl2 1058 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ 𝐵) |
17 | | simpr 476 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
18 | 16, 17 | sseldd 3569 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
19 | | simpl1r 1106 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐻) |
20 | | dihglblem.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
21 | 1, 20 | lhpbase 34302 |
. . . . 5
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
22 | 19, 21 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝑊 ∈ 𝐵) |
23 | | dihglblem.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
24 | 1, 23 | latmcl 16875 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑥 ∧ 𝑊) ∈ 𝐵) |
25 | 6, 18, 22, 24 | syl3anc 1318 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ 𝑊) ∈ 𝐵) |
26 | 4, 8 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ CLat) |
27 | | eqidd 2611 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ 𝑊) = (𝑥 ∧ 𝑊)) |
28 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑣 = 𝑥 → (𝑣 ∧ 𝑊) = (𝑥 ∧ 𝑊)) |
29 | 28 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑣 = 𝑥 → ((𝑥 ∧ 𝑊) = (𝑣 ∧ 𝑊) ↔ (𝑥 ∧ 𝑊) = (𝑥 ∧ 𝑊))) |
30 | 29 | rspcev 3282 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑆 ∧ (𝑥 ∧ 𝑊) = (𝑥 ∧ 𝑊)) → ∃𝑣 ∈ 𝑆 (𝑥 ∧ 𝑊) = (𝑣 ∧ 𝑊)) |
31 | 17, 27, 30 | syl2anc 691 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → ∃𝑣 ∈ 𝑆 (𝑥 ∧ 𝑊) = (𝑣 ∧ 𝑊)) |
32 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑢 = (𝑥 ∧ 𝑊) → (𝑢 = (𝑣 ∧ 𝑊) ↔ (𝑥 ∧ 𝑊) = (𝑣 ∧ 𝑊))) |
33 | 32 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑢 = (𝑥 ∧ 𝑊) → (∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊) ↔ ∃𝑣 ∈ 𝑆 (𝑥 ∧ 𝑊) = (𝑣 ∧ 𝑊))) |
34 | 33 | elrab 3331 |
. . . . . 6
⊢ ((𝑥 ∧ 𝑊) ∈ {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} ↔ ((𝑥 ∧ 𝑊) ∈ 𝐵 ∧ ∃𝑣 ∈ 𝑆 (𝑥 ∧ 𝑊) = (𝑣 ∧ 𝑊))) |
35 | 25, 31, 34 | sylanbrc 695 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ 𝑊) ∈ {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)}) |
36 | 35, 10 | syl6eleqr 2699 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ 𝑊) ∈ 𝑇) |
37 | 1, 2, 3 | clatglble 16948 |
. . . . 5
⊢ ((𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ (𝑥 ∧ 𝑊) ∈ 𝑇) → (𝐺‘𝑇) ≤ (𝑥 ∧ 𝑊)) |
38 | 12, 37 | mp3an2 1404 |
. . . 4
⊢ ((𝐾 ∈ CLat ∧ (𝑥 ∧ 𝑊) ∈ 𝑇) → (𝐺‘𝑇) ≤ (𝑥 ∧ 𝑊)) |
39 | 26, 36, 38 | syl2anc 691 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑇) ≤ (𝑥 ∧ 𝑊)) |
40 | 1, 2, 23 | latmle1 16899 |
. . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑥 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑥 ∧ 𝑊) ≤ 𝑥) |
41 | 6, 18, 22, 40 | syl3anc 1318 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∧ 𝑊) ≤ 𝑥) |
42 | 1, 2, 6, 15, 25, 18, 39, 41 | lattrd 16881 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑇) ≤ 𝑥) |
43 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑢 = 𝑤 → (𝑢 = (𝑣 ∧ 𝑊) ↔ 𝑤 = (𝑣 ∧ 𝑊))) |
44 | 43 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑢 = 𝑤 → (∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊) ↔ ∃𝑣 ∈ 𝑆 𝑤 = (𝑣 ∧ 𝑊))) |
45 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → (𝑣 ∧ 𝑊) = (𝑦 ∧ 𝑊)) |
46 | 45 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (𝑤 = (𝑣 ∧ 𝑊) ↔ 𝑤 = (𝑦 ∧ 𝑊))) |
47 | 46 | cbvrexv 3148 |
. . . . . . 7
⊢
(∃𝑣 ∈
𝑆 𝑤 = (𝑣 ∧ 𝑊) ↔ ∃𝑦 ∈ 𝑆 𝑤 = (𝑦 ∧ 𝑊)) |
48 | 44, 47 | syl6bb 275 |
. . . . . 6
⊢ (𝑢 = 𝑤 → (∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊) ↔ ∃𝑦 ∈ 𝑆 𝑤 = (𝑦 ∧ 𝑊))) |
49 | 48, 10 | elrab2 3333 |
. . . . 5
⊢ (𝑤 ∈ 𝑇 ↔ (𝑤 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝑆 𝑤 = (𝑦 ∧ 𝑊))) |
50 | | simp3 1056 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
51 | | simp13 1086 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) |
52 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑧 ≤ 𝑥 ↔ 𝑧 ≤ 𝑦)) |
53 | 52 | rspcva 3280 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → 𝑧 ≤ 𝑦) |
54 | 50, 51, 53 | syl2anc 691 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑧 ≤ 𝑦) |
55 | | simp11l 1165 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → 𝐾 ∈ HL) |
56 | 55 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ HL) |
57 | 56, 5 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ Lat) |
58 | | simp12 1085 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑧 ∈ 𝐵) |
59 | 56, 8 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝐾 ∈ CLat) |
60 | | simp112 1184 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑆 ⊆ 𝐵) |
61 | 1, 3 | clatglbcl 16937 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) ∈ 𝐵) |
62 | 59, 60, 61 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑆) ∈ 𝐵) |
63 | | simp11r 1166 |
. . . . . . . . . . . . 13
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → 𝑊 ∈ 𝐻) |
64 | 63 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑊 ∈ 𝐻) |
65 | 64, 21 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑊 ∈ 𝐵) |
66 | 1, 2, 3 | clatleglb 16949 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ CLat ∧ 𝑧 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵) → (𝑧 ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥)) |
67 | 59, 58, 60, 66 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → (𝑧 ≤ (𝐺‘𝑆) ↔ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥)) |
68 | 51, 67 | mpbird 246 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑧 ≤ (𝐺‘𝑆)) |
69 | | simp113 1185 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → (𝐺‘𝑆) ≤ 𝑊) |
70 | 1, 2, 57, 58, 62, 65, 68, 69 | lattrd 16881 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑧 ≤ 𝑊) |
71 | 60, 50 | sseldd 3569 |
. . . . . . . . . . 11
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝐵) |
72 | 1, 2, 23 | latlem12 16901 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Lat ∧ (𝑧 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑧 ≤ 𝑦 ∧ 𝑧 ≤ 𝑊) ↔ 𝑧 ≤ (𝑦 ∧ 𝑊))) |
73 | 57, 58, 71, 65, 72 | syl13anc 1320 |
. . . . . . . . . 10
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → ((𝑧 ≤ 𝑦 ∧ 𝑧 ≤ 𝑊) ↔ 𝑧 ≤ (𝑦 ∧ 𝑊))) |
74 | 54, 70, 73 | mpbi2and 958 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝑆) → 𝑧 ≤ (𝑦 ∧ 𝑊)) |
75 | 74 | 3expia 1259 |
. . . . . . . 8
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵) → (𝑦 ∈ 𝑆 → 𝑧 ≤ (𝑦 ∧ 𝑊))) |
76 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑤 = (𝑦 ∧ 𝑊) → (𝑧 ≤ 𝑤 ↔ 𝑧 ≤ (𝑦 ∧ 𝑊))) |
77 | 76 | biimprcd 239 |
. . . . . . . 8
⊢ (𝑧 ≤ (𝑦 ∧ 𝑊) → (𝑤 = (𝑦 ∧ 𝑊) → 𝑧 ≤ 𝑤)) |
78 | 75, 77 | syl6 34 |
. . . . . . 7
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵) → (𝑦 ∈ 𝑆 → (𝑤 = (𝑦 ∧ 𝑊) → 𝑧 ≤ 𝑤))) |
79 | 78 | rexlimdv 3012 |
. . . . . 6
⊢
(((((𝐾 ∈ HL
∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑤 ∈ 𝐵) → (∃𝑦 ∈ 𝑆 𝑤 = (𝑦 ∧ 𝑊) → 𝑧 ≤ 𝑤)) |
80 | 79 | expimpd 627 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → ((𝑤 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝑆 𝑤 = (𝑦 ∧ 𝑊)) → 𝑧 ≤ 𝑤)) |
81 | 49, 80 | syl5bi 231 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → (𝑤 ∈ 𝑇 → 𝑧 ≤ 𝑤)) |
82 | 81 | ralrimiv 2948 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → ∀𝑤 ∈ 𝑇 𝑧 ≤ 𝑤) |
83 | 55, 8 | syl 17 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → 𝐾 ∈ CLat) |
84 | | simp2 1055 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → 𝑧 ∈ 𝐵) |
85 | 1, 2, 3 | clatleglb 16949 |
. . . . 5
⊢ ((𝐾 ∈ CLat ∧ 𝑧 ∈ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑧 ≤ (𝐺‘𝑇) ↔ ∀𝑤 ∈ 𝑇 𝑧 ≤ 𝑤)) |
86 | 12, 85 | mp3an3 1405 |
. . . 4
⊢ ((𝐾 ∈ CLat ∧ 𝑧 ∈ 𝐵) → (𝑧 ≤ (𝐺‘𝑇) ↔ ∀𝑤 ∈ 𝑇 𝑧 ≤ 𝑤)) |
87 | 83, 84, 86 | syl2anc 691 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → (𝑧 ≤ (𝐺‘𝑇) ↔ ∀𝑤 ∈ 𝑇 𝑧 ≤ 𝑤)) |
88 | 82, 87 | mpbird 246 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) ∧ 𝑧 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 𝑧 ≤ 𝑥) → 𝑧 ≤ (𝐺‘𝑇)) |
89 | | simp2 1055 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) → 𝑆 ⊆ 𝐵) |
90 | 1, 2, 3, 42, 88, 9, 89, 14 | isglbd 16940 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐺‘𝑆) = (𝐺‘𝑇)) |