Theorem 0opn

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

	Ref	Expression
Assertion	0opn	$$⊢J\in \mathrm{Top}\to \varnothing \in J$$

Proof

Step	Hyp	Ref	Expression
1		uni0	$$⊢\bigcup \varnothing =\varnothing$$
2		0ss	$$⊢\varnothing \subseteq J$$
3		uniopn	$$⊢\left(J\in \mathrm{Top}\wedge \varnothing \subseteq J\right)\to \bigcup \varnothing \in J$$
4	2 3	mpan2	$$⊢J\in \mathrm{Top}\to \bigcup \varnothing \in J$$
5	1 4	eqeltrrid	$$⊢J\in \mathrm{Top}\to \varnothing \in J$$