Theorem glbeldm

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	glbeldm.b	$$⊢B={\mathrm{Base}}_K$$
	glbeldm.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	glbeldm.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	glbeldm.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)$$
	glbeldm.k	$$⊢\phi \to K\in V$$
Assertion	glbeldm	$$⊢\phi \to \left(S\in \mathrm{dom}G\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		glbeldm.b	$$⊢B={\mathrm{Base}}_K$$
2		glbeldm.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		glbeldm.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		glbeldm.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		glbeldm.k	$$⊢\phi \to K\in V$$
6		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)$$
7	1 2 3 6 5	glbdm	$$⊢\phi \to \mathrm{dom}G=\left\{s\in 𝒫B|\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\}$$
8	7	eleq2d	$$⊢\phi \to \left(S\in \mathrm{dom}G\leftrightarrow S\in \left\{s\in 𝒫B|\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)$$
9		raleq	$$⊢s=S\to \left(\forall y\in sx\underset{\dot{}}{\le }y\leftrightarrow \forall y\in Sx\underset{\dot{}}{\le }y\right)$$
10		raleq	$$⊢s=S\to \left(\forall y\in sz\underset{\dot{}}{\le }y\leftrightarrow \forall y\in Sz\underset{\dot{}}{\le }y\right)$$
11	10	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)$$
12	11	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)$$
13	9 12	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)$$
14	13	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\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)$$
15	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)$$
16	14 15	bitr4di	$$⊢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)$$
17	16	elrab	$$⊢S\in \left\{s\in 𝒫B|\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\}\leftrightarrow \left(S\in 𝒫B\wedge \exists !x\in B\psi \right)$$
18	1	fvexi	$$⊢B\in \mathrm{V}$$
19	18	elpw2	$$⊢S\in 𝒫B\leftrightarrow S\subseteq B$$
20	19	anbi1i	$$⊢\left(S\in 𝒫B\wedge \exists !x\in B\psi \right)\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)$$
21	17 20	bitri	$$⊢S\in \left\{s\in 𝒫B|\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\}\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)$$
22	8 21	bitrdi	$$⊢\phi \to \left(S\in \mathrm{dom}G\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)\right)$$