Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Atomic lattices with covering property
df-ats
Next ⟩
cvrfval
Metamath Proof Explorer
Ascii
Unicode
Definition
df-ats
Description:
Define the class of poset atoms.
(Contributed by
NM
, 18-Sep-2011)
Ref
Expression
Assertion
df-ats
⊢
Atoms
=
p
∈
V
⟼
a
∈
Base
p
|
0.
⁡
p
⋖
p
a
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
catm
class
Atoms
1
vp
setvar
p
2
cvv
class
V
3
va
setvar
a
4
cbs
class
Base
5
1
cv
setvar
p
6
5
4
cfv
class
Base
p
7
cp0
class
0.
8
5
7
cfv
class
0.
⁡
p
9
ccvr
class
⋖
10
5
9
cfv
class
⋖
p
11
3
cv
setvar
a
12
8
11
10
wbr
wff
0.
⁡
p
⋖
p
a
13
12
3
6
crab
class
a
∈
Base
p
|
0.
⁡
p
⋖
p
a
14
1
2
13
cmpt
class
p
∈
V
⟼
a
∈
Base
p
|
0.
⁡
p
⋖
p
a
15
0
14
wceq
wff
Atoms
=
p
∈
V
⟼
a
∈
Base
p
|
0.
⁡
p
⋖
p
a