Theorem topontopi

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

	Ref	Expression
Hypothesis	topontopi.1	$$⊢J\in \mathrm{TopOn}\left(B\right)$$
Assertion	topontopi	$$⊢J\in \mathrm{Top}$$

Proof

Step	Hyp	Ref	Expression
1		topontopi.1	$$⊢J\in \mathrm{TopOn}\left(B\right)$$
2		topontop	$$⊢J\in \mathrm{TopOn}\left(B\right)\to J\in \mathrm{Top}$$
3	1 2	ax-mp	$$⊢J\in \mathrm{Top}$$