Description: The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | glbc.b | |
|
glbc.g | |
||
glbc.k | |
||
glbc.s | |
||
Assertion | glbcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | glbc.b | |
|
2 | glbc.g | |
|
3 | glbc.k | |
|
4 | glbc.s | |
|
5 | eqid | |
|
6 | biid | |
|
7 | 1 5 2 3 4 | glbelss | |
8 | 1 5 2 6 3 7 | glbval | |
9 | 1 5 2 6 3 4 | glbeu | |
10 | riotacl | |
|
11 | 9 10 | syl | |
12 | 8 11 | eqeltrd | |