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 → ∅ ∈ 𝐽 )