Theorem mrelatglbALT

Description: Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015) (Proof shortened by Zhi Wang, 29-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mreclatGOOD.i	$$⊢I=\mathrm{toInc}\left(C\right)$$
	mrelatglbALT.g	$$⊢G=\mathrm{glb}\left(I\right)$$
Assertion	mrelatglbALT	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq C\wedge U\ne \varnothing \right)\to G\left(U\right)=\bigcap U$$

Proof

Step	Hyp	Ref	Expression
1		mreclatGOOD.i	$$⊢I=\mathrm{toInc}\left(C\right)$$
2		mrelatglbALT.g	$$⊢G=\mathrm{glb}\left(I\right)$$
3		simp1	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq C\wedge U\ne \varnothing \right)\to C\in \mathrm{Moore}\left(X\right)$$
4		simp2	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq C\wedge U\ne \varnothing \right)\to U\subseteq C$$
5	2	a1i	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq C\wedge U\ne \varnothing \right)\to G=\mathrm{glb}\left(I\right)$$
6		mreintcl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq C\wedge U\ne \varnothing \right)\to \bigcap U\in C$$
7		unimax	$$⊢\bigcap U\in C\to \bigcup \left\{x\in C|x\subseteq \bigcap U\right\}=\bigcap U$$
8	7	eqcomd	$$⊢\bigcap U\in C\to \bigcap U=\bigcup \left\{x\in C|x\subseteq \bigcap U\right\}$$
9	6 8	syl	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq C\wedge U\ne \varnothing \right)\to \bigcap U=\bigcup \left\{x\in C|x\subseteq \bigcap U\right\}$$
10	1 3 4 5 9 6	ipoglb	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge U\subseteq C\wedge U\ne \varnothing \right)\to G\left(U\right)=\bigcap U$$