Theorem toplatglb0

Description: The empty intersection in a topology is realized by the base set. (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}$$
	toplatglb0.g	$$⊢G=\mathrm{glb}\left(I\right)$$
Assertion	toplatglb0	$$⊢\phi \to G\left(\varnothing \right)=\bigcup J$$

Proof

Step	Hyp	Ref	Expression
1		topclat.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
2		toplatlub.j	$$⊢\phi \to J\in \mathrm{Top}$$
3		toplatglb0.g	$$⊢G=\mathrm{glb}\left(I\right)$$
4	3	a1i	$$⊢\phi \to G=\mathrm{glb}\left(I\right)$$
5		eqid	$$⊢\bigcup J=\bigcup J$$
6	5	topopn	$$⊢J\in \mathrm{Top}\to \bigcup J\in J$$
7	2 6	syl	$$⊢\phi \to \bigcup J\in J$$
8	1 4 7	ipoglb0	$$⊢\phi \to G\left(\varnothing \right)=\bigcup J$$