Theorem glbval

Description: Value of the greatest lower 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 on both sides of the equality. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	glbval.b	$$⊢B={\mathrm{Base}}_K$$
	glbval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	glbval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	glbval.p	$$⊢\psi \leftrightarrow \left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
	glbva.k	$$⊢\phi \to K\in V$$
	glbval.ss	$$⊢\phi \to S\subseteq B$$
Assertion	glbval	$$⊢\phi \to G\left(S\right)=\left(\iota x\in B|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		glbval.b	$$⊢B={\mathrm{Base}}_K$$
2		glbval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		glbval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		glbval.p	$$⊢\psi \leftrightarrow \left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
5		glbva.k	$$⊢\phi \to K\in V$$
6		glbval.ss	$$⊢\phi \to S\subseteq B$$
7		biid	$$⊢\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
8	5	adantr	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\right)\to K\in V$$
9	1 2 3 7 8	glbfval	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\right)\to G={\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right\}}$$
10	9	fveq1d	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\right)\to G\left(S\right)=\left({\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right\}}\right)\left(S\right)$$
11		simpr	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\right)\to S\in \mathrm{dom}G$$
12	1 2 3 4 8 11	glbeu	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\right)\to \exists !x\in B\psi$$
13		raleq	$$⊢s=S\to \left(\forall y\in sx\underset{\dot{}}{\le }y\leftrightarrow \forall y\in Sx\underset{\dot{}}{\le }y\right)$$
14		raleq	$$⊢s=S\to \left(\forall y\in sz\underset{\dot{}}{\le }y\leftrightarrow \forall y\in Sz\underset{\dot{}}{\le }y\right)$$
15	14	imbi1d	$$⊢s=S\to \left(\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\leftrightarrow \left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
16	15	ralbidv	$$⊢s=S\to \left(\forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\leftrightarrow \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
17	13 16	anbi12d	$$⊢s=S\to \left(\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)$$
18	17 4	bitr4di	$$⊢s=S\to \left(\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \psi \right)$$
19	18	reubidv	$$⊢s=S\to \left(\exists !x\in B\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \exists !x\in B\psi \right)$$
20	11 12 19	elabd	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\right)\to S\in \left\{s|\exists !x\in B\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right\}$$
21	20	fvresd	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\right)\to \left({\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right\}}\right)\left(S\right)=\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)\right)\left(S\right)$$
22	6	adantr	$$⊢\left(\phi \wedge S\in \mathrm{dom}G\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}G\right)\to S\in 𝒫B$$
26	18	riotabidv	$$⊢s=S\to \left(\iota x\in B|\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\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 sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)\right)=\left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\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 sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\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}G\right)\to \left(s\in 𝒫B⟼\left(\iota x\in B|\left(\forall y\in sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\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}G\right)\to G\left(S\right)=\left(\iota x\in B|\psi \right)$$
32		ndmfv	$$⊢\neg S\in \mathrm{dom}G\to G\left(S\right)=\varnothing$$
33	32	adantl	$$⊢\left(\phi \wedge \neg S\in \mathrm{dom}G\right)\to G\left(S\right)=\varnothing$$
34	1 2 3 4 5	glbeldm	$$⊢\phi \to \left(S\in \mathrm{dom}G\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}G\right)$$
36	6 35	mpand	$$⊢\phi \to \left(\exists !x\in B\psi \to S\in \mathrm{dom}G\right)$$
37	36	con3dimp	$$⊢\left(\phi \wedge \neg S\in \mathrm{dom}G\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}G\right)\to \left(\iota x\in B|\psi \right)=\varnothing$$
40	33 39	eqtr4d	$$⊢\left(\phi \wedge \neg S\in \mathrm{dom}G\right)\to G\left(S\right)=\left(\iota x\in B|\psi \right)$$
41	31 40	pm2.61dan	$$⊢\phi \to G\left(S\right)=\left(\iota x\in B|\psi \right)$$