Theorem ipolub

Description: The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with S e. dom U .) Could be significantly shortened if poslubdg is in quantified form. mrelatlub could potentially be shortened using this. See mrelatlubALT . (Contributed by Zhi Wang, 28-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$$
	ipolub.u	$$⊢\phi \to U=\mathrm{lub}\left(I\right)$$
	ipolubdm.t	$$⊢\phi \to T=\bigcap \left\{x\in F|\bigcup S\subseteq x\right\}$$
	ipolub.t	$$⊢\phi \to T\in F$$
Assertion	ipolub	$$⊢\phi \to U\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		ipolub.u	$$⊢\phi \to U=\mathrm{lub}\left(I\right)$$
5		ipolubdm.t	$$⊢\phi \to T=\bigcap \left\{x\in F|\bigcup S\subseteq x\right\}$$
6		ipolub.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		breq1	$$⊢w=y\to \left(w{\le }_{I}T\leftrightarrow y{\le }_{I}T\right)$$
13		intubeu	$$⊢T\in F\to \left(\left(\bigcup S\subseteq T\wedge \forall v\in F\left(\bigcup S\subseteq v\to T\subseteq v\right)\right)\leftrightarrow T=\bigcap \left\{x\in F|\bigcup S\subseteq x\right\}\right)$$
14	13	biimpar	$$⊢\left(T\in F\wedge T=\bigcap \left\{x\in F|\bigcup S\subseteq x\right\}\right)\to \left(\bigcup S\subseteq T\wedge \forall v\in F\left(\bigcup S\subseteq v\to T\subseteq v\right)\right)$$
15	6 5 14	syl2anc	$$⊢\phi \to \left(\bigcup S\subseteq T\wedge \forall v\in F\left(\bigcup S\subseteq v\to T\subseteq v\right)\right)$$
16	1 2 3 7	ipolublem	$$⊢\left(\phi \wedge T\in F\right)\to \left(\left(\bigcup S\subseteq T\wedge \forall v\in F\left(\bigcup S\subseteq v\to T\subseteq v\right)\right)\leftrightarrow \left(\forall w\in Sw{\le }_{I}T\wedge \forall v\in F\left(\forall w\in Sw{\le }_{I}v\to T{\le }_{I}v\right)\right)\right)$$
17	6 16	mpdan	$$⊢\phi \to \left(\left(\bigcup S\subseteq T\wedge \forall v\in F\left(\bigcup S\subseteq v\to T\subseteq v\right)\right)\leftrightarrow \left(\forall w\in Sw{\le }_{I}T\wedge \forall v\in F\left(\forall w\in Sw{\le }_{I}v\to T{\le }_{I}v\right)\right)\right)$$
18	15 17	mpbid	$$⊢\phi \to \left(\forall w\in Sw{\le }_{I}T\wedge \forall v\in F\left(\forall w\in Sw{\le }_{I}v\to T{\le }_{I}v\right)\right)$$
19	18	simpld	$$⊢\phi \to \forall w\in Sw{\le }_{I}T$$
20	19	adantr	$$⊢\left(\phi \wedge y\in S\right)\to \forall w\in Sw{\le }_{I}T$$
21		simpr	$$⊢\left(\phi \wedge y\in S\right)\to y\in S$$
22	12 20 21	rspcdva	$$⊢\left(\phi \wedge y\in S\right)\to y{\le }_{I}T$$
23		breq2	$$⊢v=z\to \left(w{\le }_{I}v\leftrightarrow w{\le }_{I}z\right)$$
24	23	ralbidv	$$⊢v=z\to \left(\forall w\in Sw{\le }_{I}v\leftrightarrow \forall w\in Sw{\le }_{I}z\right)$$
25		breq1	$$⊢w=y\to \left(w{\le }_{I}z\leftrightarrow y{\le }_{I}z\right)$$
26	25	cbvralvw	$$⊢\forall w\in Sw{\le }_{I}z\leftrightarrow \forall y\in Sy{\le }_{I}z$$
27	24 26	bitrdi	$$⊢v=z\to \left(\forall w\in Sw{\le }_{I}v\leftrightarrow \forall y\in Sy{\le }_{I}z\right)$$
28		breq2	$$⊢v=z\to \left(T{\le }_{I}v\leftrightarrow T{\le }_{I}z\right)$$
29	27 28	imbi12d	$$⊢v=z\to \left(\left(\forall w\in Sw{\le }_{I}v\to T{\le }_{I}v\right)\leftrightarrow \left(\forall y\in Sy{\le }_{I}z\to T{\le }_{I}z\right)\right)$$
30	18	simprd	$$⊢\phi \to \forall v\in F\left(\forall w\in Sw{\le }_{I}v\to T{\le }_{I}v\right)$$
31	30	adantr	$$⊢\left(\phi \wedge z\in F\right)\to \forall v\in F\left(\forall w\in Sw{\le }_{I}v\to T{\le }_{I}v\right)$$
32		simpr	$$⊢\left(\phi \wedge z\in F\right)\to z\in F$$
33	29 31 32	rspcdva	$$⊢\left(\phi \wedge z\in F\right)\to \left(\forall y\in Sy{\le }_{I}z\to T{\le }_{I}z\right)$$
34	33	3impia	$$⊢\left(\phi \wedge z\in F\wedge \forall y\in Sy{\le }_{I}z\right)\to T{\le }_{I}z$$
35	7 9 4 11 3 6 22 34	poslubdg	$$⊢\phi \to U\left(S\right)=T$$