Theorem istps

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

	Ref	Expression
Hypotheses	istps.a	|- A = ( Base ` K )
	istps.j	|- J = ( TopOpen ` K )
Assertion	istps	|- ( K e. TopSp <-> J e. ( TopOn ` A ) )

Proof

Step	Hyp	Ref	Expression
1		istps.a	|- A = ( Base ` K )
2		istps.j	|- J = ( TopOpen ` K )
3		df-topsp	|- TopSp = { f | ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) ) }
4	3	eleq2i	|- ( K e. TopSp <-> K e. { f | ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) ) } )
5		topontop	|- ( J e. ( TopOn ` A ) -> J e. Top )
6		0ntop	|- -. (/) e. Top
7		fvprc	|- ( -. K e. _V -> ( TopOpen ` K ) = (/) )
8	2 7	eqtrid	|- ( -. K e. _V -> J = (/) )
9	8	eleq1d	|- ( -. K e. _V -> ( J e. Top <-> (/) e. Top ) )
10	6 9	mtbiri	|- ( -. K e. _V -> -. J e. Top )
11	10	con4i	|- ( J e. Top -> K e. _V )
12	5 11	syl	|- ( J e. ( TopOn ` A ) -> K e. _V )
13		fveq2	|- ( f = K -> ( TopOpen ` f ) = ( TopOpen ` K ) )
14	13 2	eqtr4di	|- ( f = K -> ( TopOpen ` f ) = J )
15		fveq2	|- ( f = K -> ( Base ` f ) = ( Base ` K ) )
16	15 1	eqtr4di	|- ( f = K -> ( Base ` f ) = A )
17	16	fveq2d	|- ( f = K -> ( TopOn ` ( Base ` f ) ) = ( TopOn ` A ) )
18	14 17	eleq12d	|- ( f = K -> ( ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) ) <-> J e. ( TopOn ` A ) ) )
19	12 18	elab3	|- ( K e. { f | ( TopOpen ` f ) e. ( TopOn ` ( Base ` f ) ) } <-> J e. ( TopOn ` A ) )
20	4 19	bitri	|- ( K e. TopSp <-> J e. ( TopOn ` A ) )