Theorem topontopn

Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	tsettps.a	|- A = ( Base ` K )
	tsettps.j	|- J = ( TopSet ` K )
Assertion	topontopn	|- ( J e. ( TopOn ` A ) -> J = ( TopOpen ` K ) )

Proof

Step	Hyp	Ref	Expression
1		tsettps.a	|- A = ( Base ` K )
2		tsettps.j	|- J = ( TopSet ` K )
3		toponuni	|- ( J e. ( TopOn ` A ) -> A = U. J )
4		eqimss2	|- ( A = U. J -> U. J C_ A )
5	3 4	syl	|- ( J e. ( TopOn ` A ) -> U. J C_ A )
6		sspwuni	|- ( J C_ ~P A <-> U. J C_ A )
7	5 6	sylibr	|- ( J e. ( TopOn ` A ) -> J C_ ~P A )
8	1 2	topnid	|- ( J C_ ~P A -> J = ( TopOpen ` K ) )
9	7 8	syl	|- ( J e. ( TopOn ` A ) -> J = ( TopOpen ` K ) )