Database
BASIC ORDER THEORY
Partially ordered sets (posets)
glbfun
Next ⟩
glbeldm
Metamath Proof Explorer
Ascii
Unicode
Theorem
glbfun
Description:
The GLB is a function.
(Contributed by
NM
, 9-Sep-2018)
Ref
Expression
Hypothesis
glbfun.g
⊢
G
=
glb
⁡
K
Assertion
glbfun
⊢
Fun
⁡
G
Proof
Step
Hyp
Ref
Expression
1
glbfun.g
⊢
G
=
glb
⁡
K
2
funmpt
⊢
Fun
⁡
s
∈
𝒫
Base
K
⟼
ι
x
∈
Base
K
|
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
3
funres
⊢
Fun
⁡
s
∈
𝒫
Base
K
⟼
ι
x
∈
Base
K
|
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
→
Fun
⁡
s
∈
𝒫
Base
K
⟼
ι
x
∈
Base
K
|
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
↾
s
|
∃!
x
∈
Base
K
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
4
2
3
ax-mp
⊢
Fun
⁡
s
∈
𝒫
Base
K
⟼
ι
x
∈
Base
K
|
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
↾
s
|
∃!
x
∈
Base
K
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
5
eqid
⊢
Base
K
=
Base
K
6
eqid
⊢
≤
K
=
≤
K
7
biid
⊢
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
↔
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
8
id
⊢
K
∈
V
→
K
∈
V
9
5
6
1
7
8
glbfval
⊢
K
∈
V
→
G
=
s
∈
𝒫
Base
K
⟼
ι
x
∈
Base
K
|
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
↾
s
|
∃!
x
∈
Base
K
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
10
9
funeqd
⊢
K
∈
V
→
Fun
⁡
G
↔
Fun
⁡
s
∈
𝒫
Base
K
⟼
ι
x
∈
Base
K
|
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
↾
s
|
∃!
x
∈
Base
K
∀
y
∈
s
x
≤
K
y
∧
∀
z
∈
Base
K
∀
y
∈
s
z
≤
K
y
→
z
≤
K
x
11
4
10
mpbiri
⊢
K
∈
V
→
Fun
⁡
G
12
fun0
⊢
Fun
⁡
∅
13
fvprc
⊢
¬
K
∈
V
→
glb
⁡
K
=
∅
14
1
13
syl5eq
⊢
¬
K
∈
V
→
G
=
∅
15
14
funeqd
⊢
¬
K
∈
V
→
Fun
⁡
G
↔
Fun
⁡
∅
16
12
15
mpbiri
⊢
¬
K
∈
V
→
Fun
⁡
G
17
11
16
pm2.61i
⊢
Fun
⁡
G