| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . . 5
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) | 
| 2 |  | isdlat.b | . . . . 5
⊢ 𝐵 = (Base‘𝐾) | 
| 3 | 1, 2 | eqtr4di 2795 | . . . 4
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) | 
| 4 |  | fveq2 6906 | . . . . . 6
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) | 
| 5 |  | isdlat.j | . . . . . 6
⊢  ∨ =
(join‘𝐾) | 
| 6 | 4, 5 | eqtr4di 2795 | . . . . 5
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) | 
| 7 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾)) | 
| 8 |  | isdlat.m | . . . . . . 7
⊢  ∧ =
(meet‘𝐾) | 
| 9 | 7, 8 | eqtr4di 2795 | . . . . . 6
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ ) | 
| 10 | 9 | sbceq1d 3793 | . . . . 5
⊢ (𝑘 = 𝐾 → ([(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ [ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) | 
| 11 | 6, 10 | sbceqbid 3795 | . . . 4
⊢ (𝑘 = 𝐾 → ([(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ [ ∨ / 𝑗][ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) | 
| 12 | 3, 11 | sbceqbid 3795 | . . 3
⊢ (𝑘 = 𝐾 → ([(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ [𝐵 / 𝑏][ ∨ / 𝑗][ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) | 
| 13 | 2 | fvexi 6920 | . . . 4
⊢ 𝐵 ∈ V | 
| 14 | 5 | fvexi 6920 | . . . 4
⊢  ∨ ∈
V | 
| 15 | 8 | fvexi 6920 | . . . 4
⊢  ∧ ∈
V | 
| 16 |  | raleq 3323 | . . . . . . . 8
⊢ (𝑏 = 𝐵 → (∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) | 
| 17 | 16 | raleqbi1dv 3338 | . . . . . . 7
⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) | 
| 18 | 17 | raleqbi1dv 3338 | . . . . . 6
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) | 
| 19 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → 𝑚 = ∧ ) | 
| 20 |  | eqidd 2738 | . . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → 𝑥 = 𝑥) | 
| 21 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → 𝑗 = ∨ ) | 
| 22 | 21 | oveqd 7448 | . . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑦𝑗𝑧) = (𝑦 ∨ 𝑧)) | 
| 23 | 19, 20, 22 | oveq123d 7452 | . . . . . . . . 9
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑥𝑚(𝑦𝑗𝑧)) = (𝑥 ∧ (𝑦 ∨ 𝑧))) | 
| 24 | 19 | oveqd 7448 | . . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑥𝑚𝑦) = (𝑥 ∧ 𝑦)) | 
| 25 | 19 | oveqd 7448 | . . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑥𝑚𝑧) = (𝑥 ∧ 𝑧)) | 
| 26 | 21, 24, 25 | oveq123d 7452 | . . . . . . . . 9
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))) | 
| 27 | 23, 26 | eqeq12d 2753 | . . . . . . . 8
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → ((𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | 
| 28 | 27 | ralbidv 3178 | . . . . . . 7
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) →
(∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | 
| 29 | 28 | 2ralbidv 3221 | . . . . . 6
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | 
| 30 | 18, 29 | sylan9bb 509 | . . . . 5
⊢ ((𝑏 = 𝐵 ∧ (𝑗 = ∨ ∧ 𝑚 = ∧ )) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | 
| 31 | 30 | 3impb 1115 | . . . 4
⊢ ((𝑏 = 𝐵 ∧ 𝑗 = ∨ ∧ 𝑚 = ∧ ) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | 
| 32 | 13, 14, 15, 31 | sbc3ie 3868 | . . 3
⊢
([𝐵 / 𝑏][ ∨ / 𝑗][ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))) | 
| 33 | 12, 32 | bitrdi 287 | . 2
⊢ (𝑘 = 𝐾 → ([(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) | 
| 34 |  | df-dlat 18566 | . 2
⊢ DLat =
{𝑘 ∈ Lat ∣
[(Base‘𝑘) /
𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))} | 
| 35 | 33, 34 | elrab2 3695 | 1
⊢ (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |