Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) |
2 | | isdlat.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
3 | 1, 2 | syl6eqr 2662 |
. . . 4
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) |
4 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) |
5 | | isdlat.j |
. . . . . 6
⊢ ∨ =
(join‘𝐾) |
6 | 4, 5 | syl6eqr 2662 |
. . . . 5
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) |
7 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾)) |
8 | | isdlat.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
9 | 7, 8 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ ) |
10 | 9 | sbceq1d 3407 |
. . . . 5
⊢ (𝑘 = 𝐾 → ([(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ [ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) |
11 | 6, 10 | sbceqbid 3409 |
. . . 4
⊢ (𝑘 = 𝐾 → ([(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ [ ∨ / 𝑗][ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) |
12 | 3, 11 | sbceqbid 3409 |
. . 3
⊢ (𝑘 = 𝐾 → ([(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ [𝐵 / 𝑏][ ∨ / 𝑗][ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) |
13 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝐾)
∈ V |
14 | 2, 13 | eqeltri 2684 |
. . . 4
⊢ 𝐵 ∈ V |
15 | | fvex 6113 |
. . . . 5
⊢
(join‘𝐾)
∈ V |
16 | 5, 15 | eqeltri 2684 |
. . . 4
⊢ ∨ ∈
V |
17 | | fvex 6113 |
. . . . 5
⊢
(meet‘𝐾)
∈ V |
18 | 8, 17 | eqeltri 2684 |
. . . 4
⊢ ∧ ∈
V |
19 | | raleq 3115 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) |
20 | 19 | raleqbi1dv 3123 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) |
21 | 20 | raleqbi1dv 3123 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)))) |
22 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → 𝑚 = ∧ ) |
23 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → 𝑥 = 𝑥) |
24 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → 𝑗 = ∨ ) |
25 | 24 | oveqd 6566 |
. . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑦𝑗𝑧) = (𝑦 ∨ 𝑧)) |
26 | 22, 23, 25 | oveq123d 6570 |
. . . . . . . . 9
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑥𝑚(𝑦𝑗𝑧)) = (𝑥 ∧ (𝑦 ∨ 𝑧))) |
27 | 22 | oveqd 6566 |
. . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑥𝑚𝑦) = (𝑥 ∧ 𝑦)) |
28 | 22 | oveqd 6566 |
. . . . . . . . . 10
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → (𝑥𝑚𝑧) = (𝑥 ∧ 𝑧)) |
29 | 24, 27, 28 | oveq123d 6570 |
. . . . . . . . 9
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))) |
30 | 26, 29 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) → ((𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |
31 | 30 | ralbidv 2969 |
. . . . . . 7
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) →
(∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |
32 | 31 | 2ralbidv 2972 |
. . . . . 6
⊢ ((𝑗 = ∨ ∧ 𝑚 = ∧ ) →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |
33 | 21, 32 | sylan9bb 732 |
. . . . 5
⊢ ((𝑏 = 𝐵 ∧ (𝑗 = ∨ ∧ 𝑚 = ∧ )) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |
34 | 33 | 3impb 1252 |
. . . 4
⊢ ((𝑏 = 𝐵 ∧ 𝑗 = ∨ ∧ 𝑚 = ∧ ) →
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |
35 | 14, 16, 18, 34 | sbc3ie 3474 |
. . 3
⊢
([𝐵 / 𝑏][ ∨ / 𝑗][ ∧ / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧))) |
36 | 12, 35 | syl6bb 275 |
. 2
⊢ (𝑘 = 𝐾 → ([(Base‘𝑘) / 𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |
37 | | df-dlat 17015 |
. 2
⊢ DLat =
{𝑘 ∈ Lat ∣
[(Base‘𝑘) /
𝑏][(join‘𝑘) / 𝑗][(meet‘𝑘) / 𝑚]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑚(𝑦𝑗𝑧)) = ((𝑥𝑚𝑦)𝑗(𝑥𝑚𝑧))} |
38 | 36, 37 | elrab2 3333 |
1
⊢ (𝐾 ∈ DLat ↔ (𝐾 ∈ Lat ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ∧ (𝑦 ∨ 𝑧)) = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ 𝑧)))) |