Step | Hyp | Ref
| Expression |
1 | | isclatd.k |
. 2
⊢ (𝜑 → 𝐾 ∈ Poset) |
2 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
3 | | eqid 2738 |
. . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) |
4 | | eqid 2738 |
. . . . 5
⊢
(lub‘𝐾) =
(lub‘𝐾) |
5 | | biid 260 |
. . . . 5
⊢
((∀𝑦 ∈
𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
6 | 2, 3, 4, 5, 1 | lubdm 18058 |
. . . 4
⊢ (𝜑 → dom (lub‘𝐾) = {𝑡 ∈ 𝒫 (Base‘𝐾) ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))}) |
7 | | ssrab2 4014 |
. . . 4
⊢ {𝑡 ∈ 𝒫
(Base‘𝐾) ∣
∃!𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))} ⊆ 𝒫 (Base‘𝐾) |
8 | 6, 7 | eqsstrdi 3976 |
. . 3
⊢ (𝜑 → dom (lub‘𝐾) ⊆ 𝒫
(Base‘𝐾)) |
9 | | elpwi 4544 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵) |
10 | | isclatd.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈) |
11 | 9, 10 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ dom 𝑈) |
12 | 11 | ralrimiva 3103 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝑈) |
13 | | dfss3 3910 |
. . . . 5
⊢
(𝒫 𝐵 ⊆
dom 𝑈 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝑈) |
14 | 12, 13 | sylibr 233 |
. . . 4
⊢ (𝜑 → 𝒫 𝐵 ⊆ dom 𝑈) |
15 | | isclatd.b |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
16 | 15 | pweqd 4554 |
. . . 4
⊢ (𝜑 → 𝒫 𝐵 = 𝒫 (Base‘𝐾)) |
17 | | isclatd.u |
. . . . 5
⊢ (𝜑 → 𝑈 = (lub‘𝐾)) |
18 | 17 | dmeqd 5809 |
. . . 4
⊢ (𝜑 → dom 𝑈 = dom (lub‘𝐾)) |
19 | 14, 16, 18 | 3sstr3d 3968 |
. . 3
⊢ (𝜑 → 𝒫
(Base‘𝐾) ⊆ dom
(lub‘𝐾)) |
20 | 8, 19 | eqssd 3939 |
. 2
⊢ (𝜑 → dom (lub‘𝐾) = 𝒫 (Base‘𝐾)) |
21 | | eqid 2738 |
. . . . 5
⊢
(glb‘𝐾) =
(glb‘𝐾) |
22 | | biid 260 |
. . . . 5
⊢
((∀𝑦 ∈
𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)) ↔ (∀𝑦 ∈ 𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) |
23 | 2, 3, 21, 22, 1 | glbdm 18071 |
. . . 4
⊢ (𝜑 → dom (glb‘𝐾) = {𝑡 ∈ 𝒫 (Base‘𝐾) ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))}) |
24 | | ssrab2 4014 |
. . . 4
⊢ {𝑡 ∈ 𝒫
(Base‘𝐾) ∣
∃!𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))} ⊆ 𝒫 (Base‘𝐾) |
25 | 23, 24 | eqsstrdi 3976 |
. . 3
⊢ (𝜑 → dom (glb‘𝐾) ⊆ 𝒫
(Base‘𝐾)) |
26 | | isclatd.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺) |
27 | 9, 26 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ dom 𝐺) |
28 | 27 | ralrimiva 3103 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝐺) |
29 | | dfss3 3910 |
. . . . 5
⊢
(𝒫 𝐵 ⊆
dom 𝐺 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝐺) |
30 | 28, 29 | sylibr 233 |
. . . 4
⊢ (𝜑 → 𝒫 𝐵 ⊆ dom 𝐺) |
31 | | isclatd.g |
. . . . 5
⊢ (𝜑 → 𝐺 = (glb‘𝐾)) |
32 | 31 | dmeqd 5809 |
. . . 4
⊢ (𝜑 → dom 𝐺 = dom (glb‘𝐾)) |
33 | 30, 16, 32 | 3sstr3d 3968 |
. . 3
⊢ (𝜑 → 𝒫
(Base‘𝐾) ⊆ dom
(glb‘𝐾)) |
34 | 25, 33 | eqssd 3939 |
. 2
⊢ (𝜑 → dom (glb‘𝐾) = 𝒫 (Base‘𝐾)) |
35 | 2, 4, 21 | isclat 18207 |
. . 3
⊢ (𝐾 ∈ CLat ↔ (𝐾 ∈ Poset ∧ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)))) |
36 | 35 | biimpri 227 |
. 2
⊢ ((𝐾 ∈ Poset ∧ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾))) →
𝐾 ∈
CLat) |
37 | 1, 20, 34, 36 | syl12anc 834 |
1
⊢ (𝜑 → 𝐾 ∈ CLat) |