Detailed syntax breakdown of Definition df-oml
Step | Hyp | Ref
| Expression |
1 | | coml 36812 |
. 2
class
OML |
2 | | va |
. . . . . . . 8
setvar 𝑎 |
3 | 2 | cv 1541 |
. . . . . . 7
class 𝑎 |
4 | | vb |
. . . . . . . 8
setvar 𝑏 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑏 |
6 | | vl |
. . . . . . . . 9
setvar 𝑙 |
7 | 6 | cv 1541 |
. . . . . . . 8
class 𝑙 |
8 | | cple 16675 |
. . . . . . . 8
class
le |
9 | 7, 8 | cfv 6339 |
. . . . . . 7
class
(le‘𝑙) |
10 | 3, 5, 9 | wbr 5030 |
. . . . . 6
wff 𝑎(le‘𝑙)𝑏 |
11 | | coc 16676 |
. . . . . . . . . . 11
class
oc |
12 | 7, 11 | cfv 6339 |
. . . . . . . . . 10
class
(oc‘𝑙) |
13 | 3, 12 | cfv 6339 |
. . . . . . . . 9
class
((oc‘𝑙)‘𝑎) |
14 | | cmee 17671 |
. . . . . . . . . 10
class
meet |
15 | 7, 14 | cfv 6339 |
. . . . . . . . 9
class
(meet‘𝑙) |
16 | 5, 13, 15 | co 7170 |
. . . . . . . 8
class (𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)) |
17 | | cjn 17670 |
. . . . . . . . 9
class
join |
18 | 7, 17 | cfv 6339 |
. . . . . . . 8
class
(join‘𝑙) |
19 | 3, 16, 18 | co 7170 |
. . . . . . 7
class (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))) |
20 | 5, 19 | wceq 1542 |
. . . . . 6
wff 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))) |
21 | 10, 20 | wi 4 |
. . . . 5
wff (𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)))) |
22 | | cbs 16586 |
. . . . . 6
class
Base |
23 | 7, 22 | cfv 6339 |
. . . . 5
class
(Base‘𝑙) |
24 | 21, 4, 23 | wral 3053 |
. . . 4
wff
∀𝑏 ∈
(Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)))) |
25 | 24, 2, 23 | wral 3053 |
. . 3
wff
∀𝑎 ∈
(Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎)))) |
26 | | col 36811 |
. . 3
class
OL |
27 | 25, 6, 26 | crab 3057 |
. 2
class {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))} |
28 | 1, 27 | wceq 1542 |
1
wff OML =
{𝑙 ∈ OL ∣
∀𝑎 ∈
(Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))} |