Theorem ipoglb

Description: The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with S e. dom G .) Could be significantly shortened if posglbdg is in quantified form. mrelatglb could potentially be shortened using this. See mrelatglbALT . (Contributed by Zhi Wang, 29-Sep-2024)

	Ref	Expression
Hypotheses	ipolub.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
	ipolub.f	$$⊢\phi \to F\in V$$
	ipolub.s	$$⊢\phi \to S\subseteq F$$
	ipoglb.g	$$⊢\phi \to G=\mathrm{glb}\left(I\right)$$
	ipoglbdm.t	$$⊢\phi \to T=\bigcup \left\{x\in F|x\subseteq \bigcap S\right\}$$
	ipoglb.t	$$⊢\phi \to T\in F$$
Assertion	ipoglb	$$⊢\phi \to G\left(S\right)=T$$

Proof

Step	Hyp	Ref	Expression
1		ipolub.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		ipolub.f	$$⊢\phi \to F\in V$$
3		ipolub.s	$$⊢\phi \to S\subseteq F$$
4		ipoglb.g	$$⊢\phi \to G=\mathrm{glb}\left(I\right)$$
5		ipoglbdm.t	$$⊢\phi \to T=\bigcup \left\{x\in F|x\subseteq \bigcap S\right\}$$
6		ipoglb.t	$$⊢\phi \to T\in F$$
7		eqid	$$⊢{\le }_I={\le }_I$$
8	1	ipobas	$$⊢F\in V\to F={\mathrm{Base}}_I$$
9	2 8	syl	$$⊢\phi \to F={\mathrm{Base}}_I$$
10	1	ipopos	$$⊢I\in \mathrm{Poset}$$
11	10	a1i	$$⊢\phi \to I\in \mathrm{Poset}$$
12		breq2	$$⊢y=v\to \left(T{\le }_{I}y\leftrightarrow T{\le }_{I}v\right)$$
13		unilbeu	$$⊢T\in F\to \left(\left(T\subseteq \bigcap S\wedge \forall z\in F\left(z\subseteq \bigcap S\to z\subseteq T\right)\right)\leftrightarrow T=\bigcup \left\{x\in F|x\subseteq \bigcap S\right\}\right)$$
14	13	biimpar	$$⊢\left(T\in F\wedge T=\bigcup \left\{x\in F|x\subseteq \bigcap S\right\}\right)\to \left(T\subseteq \bigcap S\wedge \forall z\in F\left(z\subseteq \bigcap S\to z\subseteq T\right)\right)$$
15	6 5 14	syl2anc	$$⊢\phi \to \left(T\subseteq \bigcap S\wedge \forall z\in F\left(z\subseteq \bigcap S\to z\subseteq T\right)\right)$$
16	1 2 3 7	ipoglblem	$$⊢\left(\phi \wedge T\in F\right)\to \left(\left(T\subseteq \bigcap S\wedge \forall z\in F\left(z\subseteq \bigcap S\to z\subseteq T\right)\right)\leftrightarrow \left(\forall y\in ST{\le }_{I}y\wedge \forall z\in F\left(\forall y\in Sz{\le }_{I}y\to z{\le }_{I}T\right)\right)\right)$$
17	6 16	mpdan	$$⊢\phi \to \left(\left(T\subseteq \bigcap S\wedge \forall z\in F\left(z\subseteq \bigcap S\to z\subseteq T\right)\right)\leftrightarrow \left(\forall y\in ST{\le }_{I}y\wedge \forall z\in F\left(\forall y\in Sz{\le }_{I}y\to z{\le }_{I}T\right)\right)\right)$$
18	15 17	mpbid	$$⊢\phi \to \left(\forall y\in ST{\le }_{I}y\wedge \forall z\in F\left(\forall y\in Sz{\le }_{I}y\to z{\le }_{I}T\right)\right)$$
19	18	simpld	$$⊢\phi \to \forall y\in ST{\le }_{I}y$$
20	19	adantr	$$⊢\left(\phi \wedge v\in S\right)\to \forall y\in ST{\le }_{I}y$$
21		simpr	$$⊢\left(\phi \wedge v\in S\right)\to v\in S$$
22	12 20 21	rspcdva	$$⊢\left(\phi \wedge v\in S\right)\to T{\le }_{I}v$$
23		breq1	$$⊢z=w\to \left(z{\le }_{I}y\leftrightarrow w{\le }_{I}y\right)$$
24	23	ralbidv	$$⊢z=w\to \left(\forall y\in Sz{\le }_{I}y\leftrightarrow \forall y\in Sw{\le }_{I}y\right)$$
25		breq2	$$⊢y=v\to \left(w{\le }_{I}y\leftrightarrow w{\le }_{I}v\right)$$
26	25	cbvralvw	$$⊢\forall y\in Sw{\le }_{I}y\leftrightarrow \forall v\in Sw{\le }_{I}v$$
27	24 26	bitrdi	$$⊢z=w\to \left(\forall y\in Sz{\le }_{I}y\leftrightarrow \forall v\in Sw{\le }_{I}v\right)$$
28		breq1	$$⊢z=w\to \left(z{\le }_{I}T\leftrightarrow w{\le }_{I}T\right)$$
29	27 28	imbi12d	$$⊢z=w\to \left(\left(\forall y\in Sz{\le }_{I}y\to z{\le }_{I}T\right)\leftrightarrow \left(\forall v\in Sw{\le }_{I}v\to w{\le }_{I}T\right)\right)$$
30	18	simprd	$$⊢\phi \to \forall z\in F\left(\forall y\in Sz{\le }_{I}y\to z{\le }_{I}T\right)$$
31	30	adantr	$$⊢\left(\phi \wedge w\in F\right)\to \forall z\in F\left(\forall y\in Sz{\le }_{I}y\to z{\le }_{I}T\right)$$
32		simpr	$$⊢\left(\phi \wedge w\in F\right)\to w\in F$$
33	29 31 32	rspcdva	$$⊢\left(\phi \wedge w\in F\right)\to \left(\forall v\in Sw{\le }_{I}v\to w{\le }_{I}T\right)$$
34	33	3impia	$$⊢\left(\phi \wedge w\in F\wedge \forall v\in Sw{\le }_{I}v\right)\to w{\le }_{I}T$$
35	7 9 4 11 3 6 22 34	posglbdg	$$⊢\phi \to G\left(S\right)=T$$