Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Posets
meetcl
Next ⟩
meetdmss
Metamath Proof Explorer
Ascii
Unicode
Theorem
meetcl
Description:
Closure of meet of elements in the domain.
(Contributed by
NM
, 12-Sep-2018)
Ref
Expression
Hypotheses
meetcl.b
⊢
B
=
Base
K
meetcl.m
⊢
∧
˙
=
meet
⁡
K
meetcl.k
⊢
φ
→
K
∈
V
meetcl.x
⊢
φ
→
X
∈
B
meetcl.y
⊢
φ
→
Y
∈
B
meetcl.e
⊢
φ
→
X
Y
∈
dom
⁡
∧
˙
Assertion
meetcl
⊢
φ
→
X
∧
˙
Y
∈
B
Proof
Step
Hyp
Ref
Expression
1
meetcl.b
⊢
B
=
Base
K
2
meetcl.m
⊢
∧
˙
=
meet
⁡
K
3
meetcl.k
⊢
φ
→
K
∈
V
4
meetcl.x
⊢
φ
→
X
∈
B
5
meetcl.y
⊢
φ
→
Y
∈
B
6
meetcl.e
⊢
φ
→
X
Y
∈
dom
⁡
∧
˙
7
eqid
⊢
glb
⁡
K
=
glb
⁡
K
8
7
2
3
4
5
meetval
⊢
φ
→
X
∧
˙
Y
=
glb
⁡
K
⁡
X
Y
9
7
2
3
4
5
meetdef
⊢
φ
→
X
Y
∈
dom
⁡
∧
˙
↔
X
Y
∈
dom
⁡
glb
⁡
K
10
6
9
mpbid
⊢
φ
→
X
Y
∈
dom
⁡
glb
⁡
K
11
1
7
3
10
glbcl
⊢
φ
→
glb
⁡
K
⁡
X
Y
∈
B
12
8
11
eqeltrd
⊢
φ
→
X
∧
˙
Y
∈
B