This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )