Detailed syntax breakdown of Definition df-lat
| Step | Hyp | Ref
| Expression |
| 1 | | clat 18476 |
. 2
class
Lat |
| 2 | | vp |
. . . . . . . 8
setvar 𝑝 |
| 3 | 2 | cv 1539 |
. . . . . . 7
class 𝑝 |
| 4 | | cjn 18357 |
. . . . . . 7
class
join |
| 5 | 3, 4 | cfv 6561 |
. . . . . 6
class
(join‘𝑝) |
| 6 | 5 | cdm 5685 |
. . . . 5
class dom
(join‘𝑝) |
| 7 | | cbs 17247 |
. . . . . . 7
class
Base |
| 8 | 3, 7 | cfv 6561 |
. . . . . 6
class
(Base‘𝑝) |
| 9 | 8, 8 | cxp 5683 |
. . . . 5
class
((Base‘𝑝)
× (Base‘𝑝)) |
| 10 | 6, 9 | wceq 1540 |
. . . 4
wff dom
(join‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝)) |
| 11 | | cmee 18358 |
. . . . . . 7
class
meet |
| 12 | 3, 11 | cfv 6561 |
. . . . . 6
class
(meet‘𝑝) |
| 13 | 12 | cdm 5685 |
. . . . 5
class dom
(meet‘𝑝) |
| 14 | 13, 9 | wceq 1540 |
. . . 4
wff dom
(meet‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝)) |
| 15 | 10, 14 | wa 395 |
. . 3
wff (dom
(join‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝)) ∧ dom
(meet‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝))) |
| 16 | | cpo 18353 |
. . 3
class
Poset |
| 17 | 15, 2, 16 | crab 3436 |
. 2
class {𝑝 ∈ Poset ∣ (dom
(join‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝)) ∧ dom
(meet‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝)))} |
| 18 | 1, 17 | wceq 1540 |
1
wff Lat =
{𝑝 ∈ Poset ∣
(dom (join‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝)) ∧ dom
(meet‘𝑝) =
((Base‘𝑝) ×
(Base‘𝑝)))} |