Theorem toplatglb

Description: Greatest lower bounds in a topology are realized by the interior of the intersection. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	topclat.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
	toplatlub.j	$$⊢\phi \to J\in \mathrm{Top}$$
	toplatlub.s	$$⊢\phi \to S\subseteq J$$
	toplatglb.g	$$⊢G=\mathrm{glb}\left(I\right)$$
	toplatglb.e	$$⊢\phi \to S\ne \varnothing$$
Assertion	toplatglb	$$⊢\phi \to G\left(S\right)=\mathrm{int}\left(J\right)\left(\bigcap S\right)$$

Proof

Step	Hyp	Ref	Expression
1		topclat.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
2		toplatlub.j	$$⊢\phi \to J\in \mathrm{Top}$$
3		toplatlub.s	$$⊢\phi \to S\subseteq J$$
4		toplatglb.g	$$⊢G=\mathrm{glb}\left(I\right)$$
5		toplatglb.e	$$⊢\phi \to S\ne \varnothing$$
6	4	a1i	$$⊢\phi \to G=\mathrm{glb}\left(I\right)$$
7		intssuni	$$⊢S\ne \varnothing \to \bigcap S\subseteq \bigcup S$$
8	5 7	syl	$$⊢\phi \to \bigcap S\subseteq \bigcup S$$
9	3	unissd	$$⊢\phi \to \bigcup S\subseteq \bigcup J$$
10	8 9	sstrd	$$⊢\phi \to \bigcap S\subseteq \bigcup J$$
11		eqid	$$⊢\bigcup J=\bigcup J$$
12	11	ntrval	$$⊢\left(J\in \mathrm{Top}\wedge \bigcap S\subseteq \bigcup J\right)\to \mathrm{int}\left(J\right)\left(\bigcap S\right)=\bigcup \left(J\cap 𝒫\bigcap S\right)$$
13	2 10 12	syl2anc	$$⊢\phi \to \mathrm{int}\left(J\right)\left(\bigcap S\right)=\bigcup \left(J\cap 𝒫\bigcap S\right)$$
14	2	uniexd	$$⊢\phi \to \bigcup J\in \mathrm{V}$$
15	14 10	ssexd	$$⊢\phi \to \bigcap S\in \mathrm{V}$$
16		inpw	$$⊢\bigcap S\in \mathrm{V}\to J\cap 𝒫\bigcap S=\left\{x\in J|x\subseteq \bigcap S\right\}$$
17	16	unieqd	$$⊢\bigcap S\in \mathrm{V}\to \bigcup \left(J\cap 𝒫\bigcap S\right)=\bigcup \left\{x\in J|x\subseteq \bigcap S\right\}$$
18	15 17	syl	$$⊢\phi \to \bigcup \left(J\cap 𝒫\bigcap S\right)=\bigcup \left\{x\in J|x\subseteq \bigcap S\right\}$$
19	13 18	eqtrd	$$⊢\phi \to \mathrm{int}\left(J\right)\left(\bigcap S\right)=\bigcup \left\{x\in J|x\subseteq \bigcap S\right\}$$
20	11	ntropn	$$⊢\left(J\in \mathrm{Top}\wedge \bigcap S\subseteq \bigcup J\right)\to \mathrm{int}\left(J\right)\left(\bigcap S\right)\in J$$
21	2 10 20	syl2anc	$$⊢\phi \to \mathrm{int}\left(J\right)\left(\bigcap S\right)\in J$$
22	1 2 3 6 19 21	ipoglb	$$⊢\phi \to G\left(S\right)=\mathrm{int}\left(J\right)\left(\bigcap S\right)$$