Metamath Proof Explorer


Theorem 0opn

Description: The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006)

Ref Expression
Assertion 0opn ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 uni0 ∅ = ∅
2 0ss ∅ ⊆ 𝐽
3 uniopn ( ( 𝐽 ∈ Top ∧ ∅ ⊆ 𝐽 ) → ∅ ∈ 𝐽 )
4 2 3 mpan2 ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
5 1 4 eqeltrrid ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )