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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lubval.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	lubval.p	$$⊢\psi \leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
	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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lubval.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lubval.p	$$⊢\psi \leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
5		lubval.k	$$⊢\phi \to K\in V$$
6		lubval.s	$$⊢\phi \to S\subseteq B$$
7		biid	$$⊢\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
8	5	adantr	$$⊢\left(\phi \wedge S\in \mathrm{dom}U\right)\to K\in V$$
9	1 2 3 7 8	lubfval	$$⊢\left(\phi \wedge S\in \mathrm{dom}U\right)\to U={\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}}$$
10	9	fveq1d	$$⊢\left(\phi \wedge S\in \mathrm{dom}U\right)\to U\left(S\right)=\left({\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}}\right)\left(S\right)$$
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\psi$$
13		raleq	$$⊢s=S\to \left(\forall y\in sy\underset{\dot{}}{\le }x\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }x\right)$$
14		raleq	$$⊢s=S\to \left(\forall y\in sy\underset{\dot{}}{\le }z\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }z\right)$$
15	14	imbi1d	$$⊢s=S\to \left(\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
16	15	ralbidv	$$⊢s=S\to \left(\forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
17	13 16	anbi12d	$$⊢s=S\to \left(\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
18	17 4	bitr4di	$$⊢s=S\to \left(\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \psi \right)$$
19	18	reubidv	$$⊢s=S\to \left(\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \exists !x\in B\psi \right)$$
20	11 12 19	elabd	$$⊢\left(\phi \wedge S\in \mathrm{dom}U\right)\to S\in \left\{s|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}$$
21	20	fvresd	$$⊢\left(\phi \wedge S\in \mathrm{dom}U\right)\to \left({\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right\}}\right)\left(S\right)=\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)\left(S\right)$$
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\leftrightarrow S\subseteq B$$
25	22 24	sylibr	$$⊢\left(\phi \wedge S\in \mathrm{dom}U\right)\to S\in 𝒫B$$
26	18	riotabidv	$$⊢s=S\to \left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)=\left(\iota x\in B|\psi \right)$$
27		eqid	$$⊢\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)=\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)$$
28		riotaex	$$⊢\left(\iota x\in B|\psi \right)\in \mathrm{V}$$
29	26 27 28	fvmpt	$$⊢S\in 𝒫B\to \left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)\left(S\right)=\left(\iota x\in B|\psi \right)$$
30	25 29	syl	$$⊢\left(\phi \wedge S\in \mathrm{dom}U\right)\to \left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)\left(S\right)=\left(\iota x\in B|\psi \right)$$
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	$$⊢\neg S\in \mathrm{dom}U\to U\left(S\right)=\varnothing$$
33	32	adantl	$$⊢\left(\phi \wedge \neg 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\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)\right)$$
35	34	biimprd	$$⊢\phi \to \left(\left(S\subseteq B\wedge \exists !x\in B\psi \right)\to S\in \mathrm{dom}U\right)$$
36	6 35	mpand	$$⊢\phi \to \left(\exists !x\in B\psi \to S\in \mathrm{dom}U\right)$$
37	36	con3dimp	$$⊢\left(\phi \wedge \neg S\in \mathrm{dom}U\right)\to \neg \exists !x\in B\psi$$
38		riotaund	$$⊢\neg \exists !x\in B\psi \to \left(\iota x\in B|\psi \right)=\varnothing$$
39	37 38	syl	$$⊢\left(\phi \wedge \neg S\in \mathrm{dom}U\right)\to \left(\iota x\in B|\psi \right)=\varnothing$$
40	33 39	eqtr4d	$$⊢\left(\phi \wedge \neg 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)$$