Theorem topopn

Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006)

	Ref	Expression
Hypothesis	1open.1	$$⊢X=\bigcup J$$
Assertion	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$

Proof

Step	Hyp	Ref	Expression
1		1open.1	$$⊢X=\bigcup J$$
2		ssid	$$⊢J\subseteq J$$
3		uniopn	$$⊢\left(J\in \mathrm{Top}\wedge J\subseteq J\right)\to \bigcup J\in J$$
4	2 3	mpan2	$$⊢J\in \mathrm{Top}\to \bigcup J\in J$$
5	1 4	eqeltrid	$$⊢J\in \mathrm{Top}\to X\in J$$