Theorem glbfval

Description: Value of the greatest lower function of a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

	Ref	Expression
Hypotheses	glbfval.b	$$⊢B={\mathrm{Base}}_K$$
	glbfval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	glbfval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	glbfval.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)$$
	glbfval.k	$$⊢\phi \to K\in V$$
Assertion	glbfval	$$⊢\phi \to G={\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\psi \right\}}$$

Proof

Step	Hyp	Ref	Expression
1		glbfval.b	$$⊢B={\mathrm{Base}}_K$$
2		glbfval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		glbfval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		glbfval.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		glbfval.k	$$⊢\phi \to K\in V$$
6		elex	$$⊢K\in V\to K\in \mathrm{V}$$
7		fveq2	$$⊢p=K\to {\mathrm{Base}}_p={\mathrm{Base}}_K$$
8	7 1	eqtr4di	$$⊢p=K\to {\mathrm{Base}}_p=B$$
9	8	pweqd	$$⊢p=K\to 𝒫{\mathrm{Base}}_p=𝒫B$$
10		fveq2	$$⊢p=K\to {\le }_p={\le }_K$$
11	10 2	eqtr4di	$$⊢p=K\to {\le }_p=\underset{\dot{}}{\le }$$
12	11	breqd	$$⊢p=K\to \left(x{\le }_{p}y\leftrightarrow x\underset{\dot{}}{\le }y\right)$$
13	12	ralbidv	$$⊢p=K\to \left(\forall y\in sx{\le }_{p}y\leftrightarrow \forall y\in sx\underset{\dot{}}{\le }y\right)$$
14	11	breqd	$$⊢p=K\to \left(z{\le }_{p}y\leftrightarrow z\underset{\dot{}}{\le }y\right)$$
15	14	ralbidv	$$⊢p=K\to \left(\forall y\in sz{\le }_{p}y\leftrightarrow \forall y\in sz\underset{\dot{}}{\le }y\right)$$
16	11	breqd	$$⊢p=K\to \left(z{\le }_{p}x\leftrightarrow z\underset{\dot{}}{\le }x\right)$$
17	15 16	imbi12d	$$⊢p=K\to \left(\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\leftrightarrow \left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
18	8 17	raleqbidv	$$⊢p=K\to \left(\forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\leftrightarrow \forall z\in B\left(\forall y\in sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
19	13 18	anbi12d	$$⊢p=K\to \left(\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}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)$$
20	8 19	riotaeqbidv	$$⊢p=K\to \left(\iota x\in {\mathrm{Base}}_p|\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\right)\right)=\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)$$
21	9 20	mpteq12dv	$$⊢p=K\to \left(s\in 𝒫{\mathrm{Base}}_p⟼\left(\iota x\in {\mathrm{Base}}_p|\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}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)$$
22	19	reubidv	$$⊢p=K\to \left(\exists !x\in {\mathrm{Base}}_p\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\right)\leftrightarrow \exists !x\in {\mathrm{Base}}_p\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)$$
23		reueq1	$$⊢{\mathrm{Base}}_p=B\to \left(\exists !x\in {\mathrm{Base}}_p\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\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)$$
24	8 23	syl	$$⊢p=K\to \left(\exists !x\in {\mathrm{Base}}_p\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\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)$$
25	22 24	bitrd	$$⊢p=K\to \left(\exists !x\in {\mathrm{Base}}_p\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\right)\leftrightarrow \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)$$
26	25	abbidv	$$⊢p=K\to \left\{s|\exists !x\in {\mathrm{Base}}_p\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\right)\right\}=\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\}$$
27	21 26	reseq12d	$$⊢p=K\to {\left(s\in 𝒫{\mathrm{Base}}_p⟼\left(\iota x\in {\mathrm{Base}}_p|\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in {\mathrm{Base}}_p\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\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)\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\}}$$
28		df-glb	$$⊢\mathrm{glb}=\left(p\in \mathrm{V}⟼{\left(s\in 𝒫{\mathrm{Base}}_p⟼\left(\iota x\in {\mathrm{Base}}_p|\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\right)\right)\right)\upharpoonright }_{\left\{s|\exists !x\in {\mathrm{Base}}_p\left(\forall y\in sx{\le }_{p}y\wedge \forall z\in {\mathrm{Base}}_p\left(\forall y\in sz{\le }_{p}y\to z{\le }_{p}x\right)\right)\right\}}\right)$$
29	1	fvexi	$$⊢B\in \mathrm{V}$$
30	29	pwex	$$⊢𝒫B\in \mathrm{V}$$
31	30	mptex	$$⊢\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)\in \mathrm{V}$$
32	31	resex	$$⊢{\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\}}\in \mathrm{V}$$
33	27 28 32	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{glb}\left(K\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)\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\}}$$
34	4	a1i	$$⊢x\in B\to \left(\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)\right)$$
35	34	riotabiia	$$⊢\left(\iota x\in B|\psi \right)=\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)$$
36	35	mpteq2i	$$⊢\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \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)$$
37	4	reubii	$$⊢\exists !x\in B\psi \leftrightarrow \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)$$
38	37	abbii	$$⊢\left\{s|\exists !x\in B\psi \right\}=\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\}$$
39	36 38	reseq12i	$$⊢{\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\psi \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)\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\}}$$
40	33 3 39	3eqtr4g	$$⊢K\in \mathrm{V}\to G={\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\psi \right\}}$$
41	5 6 40	3syl	$$⊢\phi \to G={\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\psi \right\}}$$