This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = ∪ 𝐽 )