Theorem toponmax

Description: The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	toponmax	$$⊢J\in \mathrm{TopOn}\left(B\right)\to B\in J$$

Proof

Step	Hyp	Ref	Expression
1		toponuni	$$⊢J\in \mathrm{TopOn}\left(B\right)\to B=\bigcup J$$
2		topontop	$$⊢J\in \mathrm{TopOn}\left(B\right)\to J\in \mathrm{Top}$$
3		eqid	$$⊢\bigcup J=\bigcup J$$
4	3	topopn	$$⊢J\in \mathrm{Top}\to \bigcup J\in J$$
5	2 4	syl	$$⊢J\in \mathrm{TopOn}\left(B\right)\to \bigcup J\in J$$
6	1 5	eqeltrd	$$⊢J\in \mathrm{TopOn}\left(B\right)\to B\in J$$