Theorem glbdm

Description: Domain of the greatest lower bound function of a poset. (Contributed 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	glbdm	$$⊢\phi \to \mathrm{dom}G=\left\{s\in 𝒫B|\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	1 2 3 4 5	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\}}$$
7	6	dmeqd	$$⊢\phi \to \mathrm{dom}G=\mathrm{dom}\left({\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\psi \right\}}\right)$$
8		riotaex	$$⊢\left(\iota x\in B|\psi \right)\in \mathrm{V}$$
9		eqid	$$⊢\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)=\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)$$
10	8 9	dmmpti	$$⊢\mathrm{dom}\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)=𝒫B$$
11	10	ineq2i	$$⊢\left\{s|\exists !x\in B\psi \right\}\cap \mathrm{dom}\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)=\left\{s|\exists !x\in B\psi \right\}\cap 𝒫B$$
12		dmres	$$⊢\mathrm{dom}\left({\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\psi \right\}}\right)=\left\{s|\exists !x\in B\psi \right\}\cap \mathrm{dom}\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)$$
13		dfrab2	$$⊢\left\{s\in 𝒫B|\exists !x\in B\psi \right\}=\left\{s|\exists !x\in B\psi \right\}\cap 𝒫B$$
14	11 12 13	3eqtr4i	$$⊢\mathrm{dom}\left({\left(s\in 𝒫B⟼\left(\iota x\in B|\psi \right)\right)\upharpoonright }_{\left\{s|\exists !x\in B\psi \right\}}\right)=\left\{s\in 𝒫B|\exists !x\in B\psi \right\}$$
15	7 14	eqtrdi	$$⊢\phi \to \mathrm{dom}G=\left\{s\in 𝒫B|\exists !x\in B\psi \right\}$$