# Metamath Proof Explorer

## Theorem posglbd

Description: Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses posglbd.l
posglbd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
posglbd.g ${⊢}{\phi }\to {G}=\mathrm{glb}\left({K}\right)$
posglbd.k ${⊢}{\phi }\to {K}\in \mathrm{Poset}$
posglbd.s ${⊢}{\phi }\to {S}\subseteq {B}$
posglbd.t ${⊢}{\phi }\to {T}\in {B}$
posglbd.lb
posglbd.gt
Assertion posglbd ${⊢}{\phi }\to {G}\left({S}\right)={T}$

### Proof

Step Hyp Ref Expression
1 posglbd.l
2 posglbd.b ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
3 posglbd.g ${⊢}{\phi }\to {G}=\mathrm{glb}\left({K}\right)$
4 posglbd.k ${⊢}{\phi }\to {K}\in \mathrm{Poset}$
5 posglbd.s ${⊢}{\phi }\to {S}\subseteq {B}$
6 posglbd.t ${⊢}{\phi }\to {T}\in {B}$
7 posglbd.lb
8 posglbd.gt
9 eqid ${⊢}\mathrm{ODual}\left({K}\right)=\mathrm{ODual}\left({K}\right)$
10 9 1 oduleval
11 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
12 9 11 odubas ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{\mathrm{ODual}\left({K}\right)}$
13 2 12 eqtrdi ${⊢}{\phi }\to {B}={\mathrm{Base}}_{\mathrm{ODual}\left({K}\right)}$
14 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
15 9 14 odulub ${⊢}{K}\in \mathrm{Poset}\to \mathrm{glb}\left({K}\right)=\mathrm{lub}\left(\mathrm{ODual}\left({K}\right)\right)$
16 4 15 syl ${⊢}{\phi }\to \mathrm{glb}\left({K}\right)=\mathrm{lub}\left(\mathrm{ODual}\left({K}\right)\right)$
17 3 16 eqtrd ${⊢}{\phi }\to {G}=\mathrm{lub}\left(\mathrm{ODual}\left({K}\right)\right)$
18 9 odupos ${⊢}{K}\in \mathrm{Poset}\to \mathrm{ODual}\left({K}\right)\in \mathrm{Poset}$
19 4 18 syl ${⊢}{\phi }\to \mathrm{ODual}\left({K}\right)\in \mathrm{Poset}$
20 vex ${⊢}{x}\in \mathrm{V}$
21 brcnvg
22 20 6 21 sylancr
25 vex ${⊢}{y}\in \mathrm{V}$
33 10 13 17 19 5 6 24 32 poslubdg ${⊢}{\phi }\to {G}\left({S}\right)={T}$