Theorem glbeldm2d

Description: Member of the domain of the greatest lower bound function of a poset. (Contributed by Zhi Wang, 29-Sep-2024)

	Ref	Expression
Hypotheses	lubeldm2d.b	$$⊢\phi \to B={\mathrm{Base}}_K$$
	lubeldm2d.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_K$$
	glbeldm2d.g	$$⊢\phi \to G=\mathrm{glb}\left(K\right)$$
	glbeldm2d.p	$$⊢\left(\phi \wedge x\in B\right)\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)$$
	glbeldm2d.k	$$⊢\phi \to K\in \mathrm{Poset}$$
Assertion	glbeldm2d	$$⊢\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		lubeldm2d.b	$$⊢\phi \to B={\mathrm{Base}}_K$$
2		lubeldm2d.l	$$⊢\phi \to \underset{\dot{}}{\le }={\le }_K$$
3		glbeldm2d.g	$$⊢\phi \to G=\mathrm{glb}\left(K\right)$$
4		glbeldm2d.p	$$⊢\left(\phi \wedge x\in B\right)\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)$$
5		glbeldm2d.k	$$⊢\phi \to K\in \mathrm{Poset}$$
6		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
7		eqid	$$⊢{\le }_K={\le }_K$$
8		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
9		biid	$$⊢\left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\leftrightarrow \left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)$$
10	6 7 8 9 5	glbeldm2	$$⊢\phi \to \left(S\in \mathrm{dom}\mathrm{glb}\left(K\right)\leftrightarrow \left(S\subseteq {\mathrm{Base}}_K\wedge \exists x\in {\mathrm{Base}}_K\left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)\right)$$
11	3	dmeqd	$$⊢\phi \to \mathrm{dom}G=\mathrm{dom}\mathrm{glb}\left(K\right)$$
12	11	eleq2d	$$⊢\phi \to \left(S\in \mathrm{dom}G\leftrightarrow S\in \mathrm{dom}\mathrm{glb}\left(K\right)\right)$$
13	1	sseq2d	$$⊢\phi \to \left(S\subseteq B\leftrightarrow S\subseteq {\mathrm{Base}}_K\right)$$
14	2	breqd	$$⊢\phi \to \left(x\underset{\dot{}}{\le }y\leftrightarrow x{\le }_{K}y\right)$$
15	14	ralbidv	$$⊢\phi \to \left(\forall y\in Sx\underset{\dot{}}{\le }y\leftrightarrow \forall y\in Sx{\le }_{K}y\right)$$
16	2	breqd	$$⊢\phi \to \left(z\underset{\dot{}}{\le }y\leftrightarrow z{\le }_{K}y\right)$$
17	16	ralbidv	$$⊢\phi \to \left(\forall y\in Sz\underset{\dot{}}{\le }y\leftrightarrow \forall y\in Sz{\le }_{K}y\right)$$
18	2	breqd	$$⊢\phi \to \left(z\underset{\dot{}}{\le }x\leftrightarrow z{\le }_{K}x\right)$$
19	17 18	imbi12d	$$⊢\phi \to \left(\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\leftrightarrow \left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)$$
20	1 19	raleqbidv	$$⊢\phi \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 {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)$$
21	15 20	anbi12d	$$⊢\phi \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{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)$$
22	21	adantr	$$⊢\left(\phi \wedge x\in B\right)\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{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)$$
23	4 22	bitrd	$$⊢\left(\phi \wedge x\in B\right)\to \left(\psi \leftrightarrow \left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)$$
24	23	pm5.32da	$$⊢\phi \to \left(\left(x\in B\wedge \psi \right)\leftrightarrow \left(x\in B\wedge \left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)\right)$$
25	1	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in {\mathrm{Base}}_K\right)$$
26	25	anbi1d	$$⊢\phi \to \left(\left(x\in B\wedge \left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)\leftrightarrow \left(x\in {\mathrm{Base}}_K\wedge \left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)\right)$$
27	24 26	bitrd	$$⊢\phi \to \left(\left(x\in B\wedge \psi \right)\leftrightarrow \left(x\in {\mathrm{Base}}_K\wedge \left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)\right)$$
28	27	rexbidv2	$$⊢\phi \to \left(\exists x\in B\psi \leftrightarrow \exists x\in {\mathrm{Base}}_K\left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)$$
29	13 28	anbi12d	$$⊢\phi \to \left(\left(S\subseteq B\wedge \exists x\in B\psi \right)\leftrightarrow \left(S\subseteq {\mathrm{Base}}_K\wedge \exists x\in {\mathrm{Base}}_K\left(\forall y\in Sx{\le }_{K}y\wedge \forall z\in {\mathrm{Base}}_K\left(\forall y\in Sz{\le }_{K}y\to z{\le }_{K}x\right)\right)\right)\right)$$
30	10 12 29	3bitr4d	$$⊢\phi \to \left(S\in \mathrm{dom}G\leftrightarrow \left(S\subseteq B\wedge \exists x\in B\psi \right)\right)$$