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	⊢ 𝐼 = ( toInc ‘ 𝐽 )
	toplatlub.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
	toplatglb0.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
Assertion	toplatglb0	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = ∪ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		topclat.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
2		toplatlub.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		toplatglb0.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
4	3	a1i	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐼 ) )
5		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
6	5	topopn	⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 )
7	2 6	syl	⊢ ( 𝜑 → ∪ 𝐽 ∈ 𝐽 )
8	1 4 7	ipoglb0	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = ∪ 𝐽 )