| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . . . 7
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 2 |  | eqid 2736 | . . . . . . 7
⊢
(join‘𝐾) =
(join‘𝐾) | 
| 3 |  | simpl 482 | . . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) →
𝐾 ∈
Poset) | 
| 4 | 1, 2, 3 | joindmss 18425 | . . . . . 6
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) → dom
(join‘𝐾) ⊆
((Base‘𝐾) ×
(Base‘𝐾))) | 
| 5 |  | relxp 5702 | . . . . . . . 8
⊢ Rel
((Base‘𝐾) ×
(Base‘𝐾)) | 
| 6 | 5 | a1i 11 | . . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) → Rel
((Base‘𝐾) ×
(Base‘𝐾))) | 
| 7 |  | opelxp 5720 | . . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) ↔ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) | 
| 8 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 9 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 10 | 8, 9 | prss 4819 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) ↔ {𝑥, 𝑦} ⊆ (Base‘𝐾)) | 
| 11 | 7, 10 | sylbb 219 | . . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → {𝑥, 𝑦} ⊆ (Base‘𝐾)) | 
| 12 |  | prex 5436 | . . . . . . . . . . . 12
⊢ {𝑥, 𝑦} ∈ V | 
| 13 | 12 | elpw 4603 | . . . . . . . . . . 11
⊢ ({𝑥, 𝑦} ∈ 𝒫 (Base‘𝐾) ↔ {𝑥, 𝑦} ⊆ (Base‘𝐾)) | 
| 14 | 11, 13 | sylibr 234 | . . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → {𝑥, 𝑦} ∈ 𝒫 (Base‘𝐾)) | 
| 15 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) →
({𝑥, 𝑦} ∈ dom (lub‘𝐾) ↔ {𝑥, 𝑦} ∈ 𝒫 (Base‘𝐾))) | 
| 16 | 14, 15 | imbitrrid 246 | . . . . . . . . 9
⊢ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) →
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → {𝑥, 𝑦} ∈ dom (lub‘𝐾))) | 
| 17 | 16 | adantl 481 | . . . . . . . 8
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) →
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → {𝑥, 𝑦} ∈ dom (lub‘𝐾))) | 
| 18 |  | eqid 2736 | . . . . . . . . 9
⊢
(lub‘𝐾) =
(lub‘𝐾) | 
| 19 | 8 | a1i 11 | . . . . . . . . 9
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) →
𝑥 ∈
V) | 
| 20 | 9 | a1i 11 | . . . . . . . . 9
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) →
𝑦 ∈
V) | 
| 21 | 18, 2, 3, 19, 20 | joindef 18422 | . . . . . . . 8
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) →
(〈𝑥, 𝑦〉 ∈ dom
(join‘𝐾) ↔
{𝑥, 𝑦} ∈ dom (lub‘𝐾))) | 
| 22 | 17, 21 | sylibrd 259 | . . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) →
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → 〈𝑥, 𝑦〉 ∈ dom (join‘𝐾))) | 
| 23 | 6, 22 | relssdv 5797 | . . . . . 6
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) →
((Base‘𝐾) ×
(Base‘𝐾)) ⊆ dom
(join‘𝐾)) | 
| 24 | 4, 23 | eqssd 4000 | . . . . 5
⊢ ((𝐾 ∈ Poset ∧ dom
(lub‘𝐾) = 𝒫
(Base‘𝐾)) → dom
(join‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾))) | 
| 25 | 24 | ex 412 | . . . 4
⊢ (𝐾 ∈ Poset → (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) → dom
(join‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾)))) | 
| 26 |  | eqid 2736 | . . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) | 
| 27 |  | simpl 482 | . . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) →
𝐾 ∈
Poset) | 
| 28 | 1, 26, 27 | meetdmss 18439 | . . . . . 6
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) → dom
(meet‘𝐾) ⊆
((Base‘𝐾) ×
(Base‘𝐾))) | 
| 29 | 5 | a1i 11 | . . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) → Rel
((Base‘𝐾) ×
(Base‘𝐾))) | 
| 30 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (dom
(glb‘𝐾) = 𝒫
(Base‘𝐾) →
({𝑥, 𝑦} ∈ dom (glb‘𝐾) ↔ {𝑥, 𝑦} ∈ 𝒫 (Base‘𝐾))) | 
| 31 | 14, 30 | imbitrrid 246 | . . . . . . . . 9
⊢ (dom
(glb‘𝐾) = 𝒫
(Base‘𝐾) →
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → {𝑥, 𝑦} ∈ dom (glb‘𝐾))) | 
| 32 | 31 | adantl 481 | . . . . . . . 8
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) →
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → {𝑥, 𝑦} ∈ dom (glb‘𝐾))) | 
| 33 |  | eqid 2736 | . . . . . . . . 9
⊢
(glb‘𝐾) =
(glb‘𝐾) | 
| 34 | 8 | a1i 11 | . . . . . . . . 9
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) →
𝑥 ∈
V) | 
| 35 | 9 | a1i 11 | . . . . . . . . 9
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) →
𝑦 ∈
V) | 
| 36 | 33, 26, 27, 34, 35 | meetdef 18436 | . . . . . . . 8
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) →
(〈𝑥, 𝑦〉 ∈ dom
(meet‘𝐾) ↔
{𝑥, 𝑦} ∈ dom (glb‘𝐾))) | 
| 37 | 32, 36 | sylibrd 259 | . . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) →
(〈𝑥, 𝑦〉 ∈ ((Base‘𝐾) × (Base‘𝐾)) → 〈𝑥, 𝑦〉 ∈ dom (meet‘𝐾))) | 
| 38 | 29, 37 | relssdv 5797 | . . . . . 6
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) →
((Base‘𝐾) ×
(Base‘𝐾)) ⊆ dom
(meet‘𝐾)) | 
| 39 | 28, 38 | eqssd 4000 | . . . . 5
⊢ ((𝐾 ∈ Poset ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) → dom
(meet‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾))) | 
| 40 | 39 | ex 412 | . . . 4
⊢ (𝐾 ∈ Poset → (dom
(glb‘𝐾) = 𝒫
(Base‘𝐾) → dom
(meet‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾)))) | 
| 41 | 25, 40 | anim12d 609 | . . 3
⊢ (𝐾 ∈ Poset → ((dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)) → (dom
(join‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾)) ∧ dom
(meet‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾))))) | 
| 42 | 41 | imdistani 568 | . 2
⊢ ((𝐾 ∈ Poset ∧ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾))) →
(𝐾 ∈ Poset ∧ (dom
(join‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾)) ∧ dom
(meet‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾))))) | 
| 43 | 1, 18, 33 | isclat 18546 | . 2
⊢ (𝐾 ∈ CLat ↔ (𝐾 ∈ Poset ∧ (dom
(lub‘𝐾) = 𝒫
(Base‘𝐾) ∧ dom
(glb‘𝐾) = 𝒫
(Base‘𝐾)))) | 
| 44 | 1, 2, 26 | islat 18479 | . 2
⊢ (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom
(join‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾)) ∧ dom
(meet‘𝐾) =
((Base‘𝐾) ×
(Base‘𝐾))))) | 
| 45 | 42, 43, 44 | 3imtr4i 292 | 1
⊢ (𝐾 ∈ CLat → 𝐾 ∈ Lat) |