Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Atomic lattices with covering property
cvlatcvr1
Next ⟩
cvlatcvr2
Metamath Proof Explorer
Ascii
Unicode
Theorem
cvlatcvr1
Description:
An atom is covered by its join with a different atom.
(Contributed by
NM
, 5-Nov-2012)
Ref
Expression
Hypotheses
cvlatcvr1.j
⊢
∨
˙
=
join
⁡
K
cvlatcvr1.c
⊢
C
=
⋖
K
cvlatcvr1.a
⊢
A
=
Atoms
⁡
K
Assertion
cvlatcvr1
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
CvLat
∧
P
∈
A
∧
Q
∈
A
→
P
≠
Q
↔
P
C
P
∨
˙
Q
Proof
Step
Hyp
Ref
Expression
1
cvlatcvr1.j
⊢
∨
˙
=
join
⁡
K
2
cvlatcvr1.c
⊢
C
=
⋖
K
3
cvlatcvr1.a
⊢
A
=
Atoms
⁡
K
4
simp13
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
CvLat
∧
P
∈
A
∧
Q
∈
A
→
K
∈
CvLat
5
cvlatl
⊢
K
∈
CvLat
→
K
∈
AtLat
6
4
5
syl
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
CvLat
∧
P
∈
A
∧
Q
∈
A
→
K
∈
AtLat
7
eqid
⊢
meet
⁡
K
=
meet
⁡
K
8
eqid
⊢
0.
⁡
K
=
0.
⁡
K
9
7
8
3
atnem0
⊢
K
∈
AtLat
∧
P
∈
A
∧
Q
∈
A
→
P
≠
Q
↔
P
meet
⁡
K
Q
=
0.
⁡
K
10
6
9
syld3an1
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
CvLat
∧
P
∈
A
∧
Q
∈
A
→
P
≠
Q
↔
P
meet
⁡
K
Q
=
0.
⁡
K
11
eqid
⊢
Base
K
=
Base
K
12
11
3
atbase
⊢
P
∈
A
→
P
∈
Base
K
13
11
1
7
8
2
3
cvlcvrp
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
CvLat
∧
P
∈
Base
K
∧
Q
∈
A
→
P
meet
⁡
K
Q
=
0.
⁡
K
↔
P
C
P
∨
˙
Q
14
12
13
syl3an2
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
CvLat
∧
P
∈
A
∧
Q
∈
A
→
P
meet
⁡
K
Q
=
0.
⁡
K
↔
P
C
P
∨
˙
Q
15
10
14
bitrd
⊢
K
∈
OML
∧
K
∈
CLat
∧
K
∈
CvLat
∧
P
∈
A
∧
Q
∈
A
→
P
≠
Q
↔
P
C
P
∨
˙
Q