| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | isclatd.k | . 2
⊢ (𝜑 → 𝐾 ∈ Poset) | 
| 2 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 3 |  | eqid 2736 | . . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(lub‘𝐾) =
(lub‘𝐾) | 
| 5 |  | biid 261 | . . . . 5
⊢
((∀𝑦 ∈
𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) | 
| 6 | 2, 3, 4, 5, 1 | lubdm 18397 | . . . 4
⊢ (𝜑 → dom (lub‘𝐾) = {𝑡 ∈ 𝒫 (Base‘𝐾) ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))}) | 
| 7 |  | ssrab2 4079 | . . . 4
⊢ {𝑡 ∈ 𝒫
(Base‘𝐾) ∣
∃!𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))} ⊆ 𝒫 (Base‘𝐾) | 
| 8 | 6, 7 | eqsstrdi 4027 | . . 3
⊢ (𝜑 → dom (lub‘𝐾) ⊆ 𝒫
(Base‘𝐾)) | 
| 9 |  | elpwi 4606 | . . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵) | 
| 10 |  | isclatd.1 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝑈) | 
| 11 | 9, 10 | sylan2 593 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ dom 𝑈) | 
| 12 | 11 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝑈) | 
| 13 |  | dfss3 3971 | . . . . 5
⊢
(𝒫 𝐵 ⊆
dom 𝑈 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝑈) | 
| 14 | 12, 13 | sylibr 234 | . . . 4
⊢ (𝜑 → 𝒫 𝐵 ⊆ dom 𝑈) | 
| 15 |  | isclatd.b | . . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) | 
| 16 | 15 | pweqd 4616 | . . . 4
⊢ (𝜑 → 𝒫 𝐵 = 𝒫 (Base‘𝐾)) | 
| 17 |  | isclatd.u | . . . . 5
⊢ (𝜑 → 𝑈 = (lub‘𝐾)) | 
| 18 | 17 | dmeqd 5915 | . . . 4
⊢ (𝜑 → dom 𝑈 = dom (lub‘𝐾)) | 
| 19 | 14, 16, 18 | 3sstr3d 4037 | . . 3
⊢ (𝜑 → 𝒫
(Base‘𝐾) ⊆ dom
(lub‘𝐾)) | 
| 20 | 8, 19 | eqssd 4000 | . 2
⊢ (𝜑 → dom (lub‘𝐾) = 𝒫 (Base‘𝐾)) | 
| 21 |  | eqid 2736 | . . . . 5
⊢
(glb‘𝐾) =
(glb‘𝐾) | 
| 22 |  | biid 261 | . . . . 5
⊢
((∀𝑦 ∈
𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)) ↔ (∀𝑦 ∈ 𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) | 
| 23 | 2, 3, 21, 22, 1 | glbdm 18410 | . . . 4
⊢ (𝜑 → dom (glb‘𝐾) = {𝑡 ∈ 𝒫 (Base‘𝐾) ∣ ∃!𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))}) | 
| 24 |  | ssrab2 4079 | . . . 4
⊢ {𝑡 ∈ 𝒫
(Base‘𝐾) ∣
∃!𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑡 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))} ⊆ 𝒫 (Base‘𝐾) | 
| 25 | 23, 24 | eqsstrdi 4027 | . . 3
⊢ (𝜑 → dom (glb‘𝐾) ⊆ 𝒫
(Base‘𝐾)) | 
| 26 |  | isclatd.2 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ⊆ 𝐵) → 𝑠 ∈ dom 𝐺) | 
| 27 | 9, 26 | sylan2 593 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ dom 𝐺) | 
| 28 | 27 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝐺) | 
| 29 |  | dfss3 3971 | . . . . 5
⊢
(𝒫 𝐵 ⊆
dom 𝐺 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ∈ dom 𝐺) | 
| 30 | 28, 29 | sylibr 234 | . . . 4
⊢ (𝜑 → 𝒫 𝐵 ⊆ dom 𝐺) | 
| 31 |  | isclatd.g | . . . . 5
⊢ (𝜑 → 𝐺 = (glb‘𝐾)) | 
| 32 | 31 | dmeqd 5915 | . . . 4
⊢ (𝜑 → dom 𝐺 = dom (glb‘𝐾)) | 
| 33 | 30, 16, 32 | 3sstr3d 4037 | . . 3
⊢ (𝜑 → 𝒫
(Base‘𝐾) ⊆ dom
(glb‘𝐾)) | 
| 34 | 25, 33 | eqssd 4000 | . 2
⊢ (𝜑 → dom (glb‘𝐾) = 𝒫 (Base‘𝐾)) | 
| 35 | 2, 4, 21 | isclat 18546 | . . 3
⊢ (𝐾 ∈ CLat ↔ (𝐾 ∈ Poset ∧ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)))) | 
| 36 | 35 | biimpri 228 | . 2
⊢ ((𝐾 ∈ Poset ∧ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾))) →
𝐾 ∈
CLat) | 
| 37 | 1, 20, 34, 36 | syl12anc 836 | 1
⊢ (𝜑 → 𝐾 ∈ CLat) |