Theorem toponuni

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

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

Proof

Step	Hyp	Ref	Expression
1		istopon	$$⊢J\in \mathrm{TopOn}\left(B\right)\leftrightarrow \left(J\in \mathrm{Top}\wedge B=\bigcup J\right)$$
2	1	simprbi	$$⊢J\in \mathrm{TopOn}\left(B\right)\to B=\bigcup J$$