# Metamath Proof Explorer

## Theorem glbfval

Description: Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

Ref Expression
Hypotheses glbfval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
glbfval.l
glbfval.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
glbfval.p
glbfval.k ${⊢}{\phi }\to {K}\in {V}$
Assertion glbfval ${⊢}{\phi }\to {G}={\left({s}\in 𝒫{B}⟼\left(\iota {x}\in {B}|{\psi }\right)\right)↾}_{\left\{{s}|\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right\}}$

### Proof

Step Hyp Ref Expression
1 glbfval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 glbfval.l
3 glbfval.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
4 glbfval.p
5 glbfval.k ${⊢}{\phi }\to {K}\in {V}$
6 elex ${⊢}{K}\in {V}\to {K}\in \mathrm{V}$
7 fveq2 ${⊢}{p}={K}\to {\mathrm{Base}}_{{p}}={\mathrm{Base}}_{{K}}$
8 7 1 eqtr4di ${⊢}{p}={K}\to {\mathrm{Base}}_{{p}}={B}$
9 8 pweqd ${⊢}{p}={K}\to 𝒫{\mathrm{Base}}_{{p}}=𝒫{B}$
10 fveq2 ${⊢}{p}={K}\to {\le }_{{p}}={\le }_{{K}}$
11 10 2 eqtr4di
12 11 breqd
13 12 ralbidv
14 11 breqd
15 14 ralbidv
16 11 breqd
17 15 16 imbi12d
18 8 17 raleqbidv
19 13 18 anbi12d
20 8 19 riotaeqbidv
21 9 20 mpteq12dv
22 19 reubidv
23 reueq1
24 8 23 syl
25 22 24 bitrd
26 25 abbidv
27 21 26 reseq12d
28 df-glb ${⊢}\mathrm{glb}=\left({p}\in \mathrm{V}⟼{\left({s}\in 𝒫{\mathrm{Base}}_{{p}}⟼\left(\iota {x}\in {\mathrm{Base}}_{{p}}|\left(\forall {y}\in {s}\phantom{\rule{.4em}{0ex}}{x}{\le }_{{p}}{y}\wedge \forall {z}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {s}\phantom{\rule{.4em}{0ex}}{z}{\le }_{{p}}{y}\to {z}{\le }_{{p}}{x}\right)\right)\right)\right)↾}_{\left\{{s}|\exists !{x}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {s}\phantom{\rule{.4em}{0ex}}{x}{\le }_{{p}}{y}\wedge \forall {z}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {s}\phantom{\rule{.4em}{0ex}}{z}{\le }_{{p}}{y}\to {z}{\le }_{{p}}{x}\right)\right)\right\}}\right)$
29 1 fvexi ${⊢}{B}\in \mathrm{V}$
30 29 pwex ${⊢}𝒫{B}\in \mathrm{V}$
31 30 mptex
32 31 resex
33 27 28 32 fvmpt
34 4 a1i
35 34 riotabiia
36 35 mpteq2i
37 4 reubii
38 37 abbii
39 36 38 reseq12i
40 33 3 39 3eqtr4g ${⊢}{K}\in \mathrm{V}\to {G}={\left({s}\in 𝒫{B}⟼\left(\iota {x}\in {B}|{\psi }\right)\right)↾}_{\left\{{s}|\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right\}}$
41 5 6 40 3syl ${⊢}{\phi }\to {G}={\left({s}\in 𝒫{B}⟼\left(\iota {x}\in {B}|{\psi }\right)\right)↾}_{\left\{{s}|\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right\}}$