Metamath Proof Explorer


Theorem glbcl

Description: The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018)

Ref Expression
Hypotheses glbc.b B=BaseK
glbc.g G=glbK
glbc.k φKV
glbc.s φSdomG
Assertion glbcl φGSB

Proof

Step Hyp Ref Expression
1 glbc.b B=BaseK
2 glbc.g G=glbK
3 glbc.k φKV
4 glbc.s φSdomG
5 eqid K=K
6 biid ySxKyzBySzKyzKxySxKyzBySzKyzKx
7 1 5 2 3 4 glbelss φSB
8 1 5 2 6 3 7 glbval φGS=ιxB|ySxKyzBySzKyzKx
9 1 5 2 6 3 4 glbeu φ∃!xBySxKyzBySzKyzKx
10 riotacl ∃!xBySxKyzBySzKyzKxιxB|ySxKyzBySzKyzKxB
11 9 10 syl φιxB|ySxKyzBySzKyzKxB
12 8 11 eqeltrd φGSB