Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihglblem2N Structured version   Visualization version   GIF version

Theorem dihglblem2N 38870
 Description: The GLB of a set of lattice elements 𝑆 is the same as that of the set 𝑇 with elements of 𝑆 cut down to be under 𝑊. (Contributed by NM, 19-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihglblem.b 𝐵 = (Base‘𝐾)
dihglblem.l = (le‘𝐾)
dihglblem.m = (meet‘𝐾)
dihglblem.g 𝐺 = (glb‘𝐾)
dihglblem.h 𝐻 = (LHyp‘𝐾)
dihglblem.t 𝑇 = {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)}
Assertion
Ref Expression
dihglblem2N (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) → (𝐺𝑆) = (𝐺𝑇))
Distinct variable groups:   𝑣,𝑢,   𝑢,𝐵   𝑢,𝑆,𝑣   𝑢,𝑊,𝑣
Allowed substitution hints:   𝐵(𝑣)   𝑇(𝑣,𝑢)   𝐺(𝑣,𝑢)   𝐻(𝑣,𝑢)   𝐾(𝑣,𝑢)   (𝑣,𝑢)

Proof of Theorem dihglblem2N
Dummy variables 𝑥 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihglblem.b . 2 𝐵 = (Base‘𝐾)
2 dihglblem.l . 2 = (le‘𝐾)
3 dihglblem.g . 2 𝐺 = (glb‘𝐾)
4 simpl1l 1221 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝐾 ∈ HL)
54hllatd 36940 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝐾 ∈ Lat)
6 simp1l 1194 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) → 𝐾 ∈ HL)
7 hlclat 36934 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ CLat)
86, 7syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) → 𝐾 ∈ CLat)
9 dihglblem.t . . . . . 6 𝑇 = {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)}
10 ssrab2 3984 . . . . . 6 {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ⊆ 𝐵
119, 10eqsstri 3926 . . . . 5 𝑇𝐵
121, 3clatglbcl 17790 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑇𝐵) → (𝐺𝑇) ∈ 𝐵)
138, 11, 12sylancl 589 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) → (𝐺𝑇) ∈ 𝐵)
1413adantr 484 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝐺𝑇) ∈ 𝐵)
15 simpl2 1189 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝑆𝐵)
16 simpr 488 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝑥𝑆)
1715, 16sseldd 3893 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝑥𝐵)
18 simpl1r 1222 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝑊𝐻)
19 dihglblem.h . . . . . 6 𝐻 = (LHyp‘𝐾)
201, 19lhpbase 37574 . . . . 5 (𝑊𝐻𝑊𝐵)
2118, 20syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝑊𝐵)
22 dihglblem.m . . . . 5 = (meet‘𝐾)
231, 22latmcl 17728 . . . 4 ((𝐾 ∈ Lat ∧ 𝑥𝐵𝑊𝐵) → (𝑥 𝑊) ∈ 𝐵)
245, 17, 21, 23syl3anc 1368 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝑥 𝑊) ∈ 𝐵)
254, 7syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → 𝐾 ∈ CLat)
26 eqidd 2759 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝑥 𝑊) = (𝑥 𝑊))
27 oveq1 7157 . . . . . . . 8 (𝑣 = 𝑥 → (𝑣 𝑊) = (𝑥 𝑊))
2827rspceeqv 3556 . . . . . . 7 ((𝑥𝑆 ∧ (𝑥 𝑊) = (𝑥 𝑊)) → ∃𝑣𝑆 (𝑥 𝑊) = (𝑣 𝑊))
2916, 26, 28syl2anc 587 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → ∃𝑣𝑆 (𝑥 𝑊) = (𝑣 𝑊))
30 eqeq1 2762 . . . . . . . 8 (𝑢 = (𝑥 𝑊) → (𝑢 = (𝑣 𝑊) ↔ (𝑥 𝑊) = (𝑣 𝑊)))
3130rexbidv 3221 . . . . . . 7 (𝑢 = (𝑥 𝑊) → (∃𝑣𝑆 𝑢 = (𝑣 𝑊) ↔ ∃𝑣𝑆 (𝑥 𝑊) = (𝑣 𝑊)))
3231elrab 3602 . . . . . 6 ((𝑥 𝑊) ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)} ↔ ((𝑥 𝑊) ∈ 𝐵 ∧ ∃𝑣𝑆 (𝑥 𝑊) = (𝑣 𝑊)))
3324, 29, 32sylanbrc 586 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝑥 𝑊) ∈ {𝑢𝐵 ∣ ∃𝑣𝑆 𝑢 = (𝑣 𝑊)})
3433, 9eleqtrrdi 2863 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝑥 𝑊) ∈ 𝑇)
351, 2, 3clatglble 17801 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑇𝐵 ∧ (𝑥 𝑊) ∈ 𝑇) → (𝐺𝑇) (𝑥 𝑊))
3611, 35mp3an2 1446 . . . 4 ((𝐾 ∈ CLat ∧ (𝑥 𝑊) ∈ 𝑇) → (𝐺𝑇) (𝑥 𝑊))
3725, 34, 36syl2anc 587 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝐺𝑇) (𝑥 𝑊))
381, 2, 22latmle1 17752 . . . 4 ((𝐾 ∈ Lat ∧ 𝑥𝐵𝑊𝐵) → (𝑥 𝑊) 𝑥)
395, 17, 21, 38syl3anc 1368 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝑥 𝑊) 𝑥)
401, 2, 5, 14, 24, 17, 37, 39lattrd 17734 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑥𝑆) → (𝐺𝑇) 𝑥)
41 eqeq1 2762 . . . . . . . 8 (𝑢 = 𝑤 → (𝑢 = (𝑣 𝑊) ↔ 𝑤 = (𝑣 𝑊)))
4241rexbidv 3221 . . . . . . 7 (𝑢 = 𝑤 → (∃𝑣𝑆 𝑢 = (𝑣 𝑊) ↔ ∃𝑣𝑆 𝑤 = (𝑣 𝑊)))
43 oveq1 7157 . . . . . . . . 9 (𝑣 = 𝑦 → (𝑣 𝑊) = (𝑦 𝑊))
4443eqeq2d 2769 . . . . . . . 8 (𝑣 = 𝑦 → (𝑤 = (𝑣 𝑊) ↔ 𝑤 = (𝑦 𝑊)))
4544cbvrexvw 3362 . . . . . . 7 (∃𝑣𝑆 𝑤 = (𝑣 𝑊) ↔ ∃𝑦𝑆 𝑤 = (𝑦 𝑊))
4642, 45bitrdi 290 . . . . . 6 (𝑢 = 𝑤 → (∃𝑣𝑆 𝑢 = (𝑣 𝑊) ↔ ∃𝑦𝑆 𝑤 = (𝑦 𝑊)))
4746, 9elrab2 3605 . . . . 5 (𝑤𝑇 ↔ (𝑤𝐵 ∧ ∃𝑦𝑆 𝑤 = (𝑦 𝑊)))
48 simp3 1135 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑦𝑆)
49 simp13 1202 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → ∀𝑥𝑆 𝑧 𝑥)
50 breq2 5036 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (𝑧 𝑥𝑧 𝑦))
5150rspcva 3539 . . . . . . . . . . 11 ((𝑦𝑆 ∧ ∀𝑥𝑆 𝑧 𝑥) → 𝑧 𝑦)
5248, 49, 51syl2anc 587 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑧 𝑦)
53 simp11l 1281 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → 𝐾 ∈ HL)
54533ad2ant1 1130 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝐾 ∈ HL)
5554hllatd 36940 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝐾 ∈ Lat)
56 simp12 1201 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑧𝐵)
5754, 7syl 17 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝐾 ∈ CLat)
58 simp112 1300 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑆𝐵)
591, 3clatglbcl 17790 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑆𝐵) → (𝐺𝑆) ∈ 𝐵)
6057, 58, 59syl2anc 587 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → (𝐺𝑆) ∈ 𝐵)
61 simp11r 1282 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → 𝑊𝐻)
62613ad2ant1 1130 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑊𝐻)
6362, 20syl 17 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑊𝐵)
641, 2, 3clatleglb 17802 . . . . . . . . . . . . 13 ((𝐾 ∈ CLat ∧ 𝑧𝐵𝑆𝐵) → (𝑧 (𝐺𝑆) ↔ ∀𝑥𝑆 𝑧 𝑥))
6557, 56, 58, 64syl3anc 1368 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → (𝑧 (𝐺𝑆) ↔ ∀𝑥𝑆 𝑧 𝑥))
6649, 65mpbird 260 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑧 (𝐺𝑆))
67 simp113 1301 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → (𝐺𝑆) 𝑊)
681, 2, 55, 56, 60, 63, 66, 67lattrd 17734 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑧 𝑊)
6958, 48sseldd 3893 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑦𝐵)
701, 2, 22latlem12 17754 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ (𝑧𝐵𝑦𝐵𝑊𝐵)) → ((𝑧 𝑦𝑧 𝑊) ↔ 𝑧 (𝑦 𝑊)))
7155, 56, 69, 63, 70syl13anc 1369 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → ((𝑧 𝑦𝑧 𝑊) ↔ 𝑧 (𝑦 𝑊)))
7252, 68, 71mpbi2and 711 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵𝑦𝑆) → 𝑧 (𝑦 𝑊))
73723expia 1118 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵) → (𝑦𝑆𝑧 (𝑦 𝑊)))
74 breq2 5036 . . . . . . . . 9 (𝑤 = (𝑦 𝑊) → (𝑧 𝑤𝑧 (𝑦 𝑊)))
7574biimprcd 253 . . . . . . . 8 (𝑧 (𝑦 𝑊) → (𝑤 = (𝑦 𝑊) → 𝑧 𝑤))
7673, 75syl6 35 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵) → (𝑦𝑆 → (𝑤 = (𝑦 𝑊) → 𝑧 𝑤)))
7776rexlimdv 3207 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) ∧ 𝑤𝐵) → (∃𝑦𝑆 𝑤 = (𝑦 𝑊) → 𝑧 𝑤))
7877expimpd 457 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → ((𝑤𝐵 ∧ ∃𝑦𝑆 𝑤 = (𝑦 𝑊)) → 𝑧 𝑤))
7947, 78syl5bi 245 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → (𝑤𝑇𝑧 𝑤))
8079ralrimiv 3112 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → ∀𝑤𝑇 𝑧 𝑤)
8153, 7syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → 𝐾 ∈ CLat)
82 simp2 1134 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → 𝑧𝐵)
831, 2, 3clatleglb 17802 . . . . 5 ((𝐾 ∈ CLat ∧ 𝑧𝐵𝑇𝐵) → (𝑧 (𝐺𝑇) ↔ ∀𝑤𝑇 𝑧 𝑤))
8411, 83mp3an3 1447 . . . 4 ((𝐾 ∈ CLat ∧ 𝑧𝐵) → (𝑧 (𝐺𝑇) ↔ ∀𝑤𝑇 𝑧 𝑤))
8581, 82, 84syl2anc 587 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → (𝑧 (𝐺𝑇) ↔ ∀𝑤𝑇 𝑧 𝑤))
8680, 85mpbird 260 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) ∧ 𝑧𝐵 ∧ ∀𝑥𝑆 𝑧 𝑥) → 𝑧 (𝐺𝑇))
87 simp2 1134 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) → 𝑆𝐵)
881, 2, 3, 40, 86, 8, 87, 13isglbd 17793 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐵 ∧ (𝐺𝑆) 𝑊) → (𝐺𝑆) = (𝐺𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  {crab 3074   ⊆ wss 3858   class class class wbr 5032  ‘cfv 6335  (class class class)co 7150  Basecbs 16541  lecple 16630  glbcglb 17619  meetcmee 17621  Latclat 17721  CLatccla 17783  HLchlt 36926  LHypclh 37560 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-poset 17622  df-lub 17650  df-glb 17651  df-join 17652  df-meet 17653  df-lat 17722  df-clat 17784  df-atl 36874  df-cvlat 36898  df-hlat 36927  df-lhyp 37564 This theorem is referenced by:  dihglblem3N  38871  dihglblem3aN  38872
 Copyright terms: Public domain W3C validator