# Metamath Proof Explorer

## Theorem glbval

Description: Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying S e. dom U ) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses glbval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
glbval.l
glbval.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
glbval.p
glbva.k ${⊢}{\phi }\to {K}\in {V}$
glbval.ss ${⊢}{\phi }\to {S}\subseteq {B}$
Assertion glbval ${⊢}{\phi }\to {G}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 glbval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 glbval.l
3 glbval.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
4 glbval.p
5 glbva.k ${⊢}{\phi }\to {K}\in {V}$
6 glbval.ss ${⊢}{\phi }\to {S}\subseteq {B}$
7 biid
8 5 adantr ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{G}\right)\to {K}\in {V}$
9 1 2 3 7 8 glbfval
10 9 fveq1d
11 simpr ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{G}\right)\to {S}\in \mathrm{dom}{G}$
12 1 2 3 4 8 11 glbeu ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{G}\right)\to \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
13 raleq
14 raleq
15 14 imbi1d
16 15 ralbidv
17 13 16 anbi12d
18 17 4 syl6bbr
19 18 reubidv
20 11 12 19 elabd
21 20 fvresd
22 6 adantr ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{G}\right)\to {S}\subseteq {B}$
23 1 fvexi ${⊢}{B}\in \mathrm{V}$
24 23 elpw2 ${⊢}{S}\in 𝒫{B}↔{S}\subseteq {B}$
25 22 24 sylibr ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{G}\right)\to {S}\in 𝒫{B}$
26 18 riotabidv
27 eqid
28 riotaex ${⊢}\left(\iota {x}\in {B}|{\psi }\right)\in \mathrm{V}$
29 26 27 28 fvmpt
30 25 29 syl
31 10 21 30 3eqtrd ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{G}\right)\to {G}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$
32 ndmfv ${⊢}¬{S}\in \mathrm{dom}{G}\to {G}\left({S}\right)=\varnothing$
33 32 adantl ${⊢}\left({\phi }\wedge ¬{S}\in \mathrm{dom}{G}\right)\to {G}\left({S}\right)=\varnothing$
34 1 2 3 4 5 glbeldm ${⊢}{\phi }\to \left({S}\in \mathrm{dom}{G}↔\left({S}\subseteq {B}\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
35 34 biimprd ${⊢}{\phi }\to \left(\left({S}\subseteq {B}\wedge \exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to {S}\in \mathrm{dom}{G}\right)$
36 6 35 mpand ${⊢}{\phi }\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\to {S}\in \mathrm{dom}{G}\right)$
37 36 con3dimp ${⊢}\left({\phi }\wedge ¬{S}\in \mathrm{dom}{G}\right)\to ¬\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$
38 riotaund ${⊢}¬\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\iota {x}\in {B}|{\psi }\right)=\varnothing$
39 37 38 syl ${⊢}\left({\phi }\wedge ¬{S}\in \mathrm{dom}{G}\right)\to \left(\iota {x}\in {B}|{\psi }\right)=\varnothing$
40 33 39 eqtr4d ${⊢}\left({\phi }\wedge ¬{S}\in \mathrm{dom}{G}\right)\to {G}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$
41 31 40 pm2.61dan ${⊢}{\phi }\to {G}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$