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 e. ( TopOn ` B )
Assertion	topontopi	|- J e. Top

Proof

Step	Hyp	Ref	Expression
1		topontopi.1	|- J e. ( TopOn ` B )
2		topontop	|- ( J e. ( TopOn ` B ) -> J e. Top )
3	1 2	ax-mp	|- J e. Top