# Metamath Proof Explorer

## Theorem lubval

Description: Value of the least upper 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. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses lubval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
lubval.l
lubval.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
lubval.p
lubval.k ${⊢}{\phi }\to {K}\in {V}$
lubval.s ${⊢}{\phi }\to {S}\subseteq {B}$
Assertion lubval ${⊢}{\phi }\to {U}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 lubval.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lubval.l
3 lubval.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
4 lubval.p
5 lubval.k ${⊢}{\phi }\to {K}\in {V}$
6 lubval.s ${⊢}{\phi }\to {S}\subseteq {B}$
7 biid
8 5 adantr ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{U}\right)\to {K}\in {V}$
9 1 2 3 7 8 lubfval
10 9 fveq1d
11 simpr ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{U}\right)\to {S}\in \mathrm{dom}{U}$
12 1 2 3 4 8 11 lubeu ${⊢}\left({\phi }\wedge {S}\in \mathrm{dom}{U}\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}{U}\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}{U}\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}{U}\right)\to {U}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$
32 ndmfv ${⊢}¬{S}\in \mathrm{dom}{U}\to {U}\left({S}\right)=\varnothing$
33 32 adantl ${⊢}\left({\phi }\wedge ¬{S}\in \mathrm{dom}{U}\right)\to {U}\left({S}\right)=\varnothing$
34 1 2 3 4 5 lubeldm ${⊢}{\phi }\to \left({S}\in \mathrm{dom}{U}↔\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}{U}\right)$
36 6 35 mpand ${⊢}{\phi }\to \left(\exists !{x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\to {S}\in \mathrm{dom}{U}\right)$
37 36 con3dimp ${⊢}\left({\phi }\wedge ¬{S}\in \mathrm{dom}{U}\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}{U}\right)\to \left(\iota {x}\in {B}|{\psi }\right)=\varnothing$
40 33 39 eqtr4d ${⊢}\left({\phi }\wedge ¬{S}\in \mathrm{dom}{U}\right)\to {U}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$
41 31 40 pm2.61dan ${⊢}{\phi }\to {U}\left({S}\right)=\left(\iota {x}\in {B}|{\psi }\right)$