MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  istps Unicode version

Theorem istps 16674
Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
Hypotheses
Ref Expression
istps.a  |-  A  =  ( Base `  K
)
istps.j  |-  J  =  ( TopOpen `  K )
Assertion
Ref Expression
istps  |-  ( K  e.  TopSp 
<->  J  e.  (TopOn `  A ) )

Proof of Theorem istps
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 df-topsp 16640 . . 3  |-  TopSp  =  {
f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f
) ) }
21eleq2i 2347 . 2  |-  ( K  e.  TopSp 
<->  K  e.  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) } )
3 topontop 16664 . . . 4  |-  ( J  e.  (TopOn `  A
)  ->  J  e.  Top )
4 0ntop 16651 . . . . . 6  |-  -.  (/)  e.  Top
5 istps.j . . . . . . . 8  |-  J  =  ( TopOpen `  K )
6 fvprc 5519 . . . . . . . 8  |-  ( -.  K  e.  _V  ->  (
TopOpen `  K )  =  (/) )
75, 6syl5eq 2327 . . . . . . 7  |-  ( -.  K  e.  _V  ->  J  =  (/) )
87eleq1d 2349 . . . . . 6  |-  ( -.  K  e.  _V  ->  ( J  e.  Top  <->  (/)  e.  Top ) )
94, 8mtbiri 294 . . . . 5  |-  ( -.  K  e.  _V  ->  -.  J  e.  Top )
109con4i 122 . . . 4  |-  ( J  e.  Top  ->  K  e.  _V )
113, 10syl 15 . . 3  |-  ( J  e.  (TopOn `  A
)  ->  K  e.  _V )
12 fveq2 5525 . . . . 5  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  ( TopOpen `  K )
)
1312, 5syl6eqr 2333 . . . 4  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  J )
14 fveq2 5525 . . . . . 6  |-  ( f  =  K  ->  ( Base `  f )  =  ( Base `  K
) )
15 istps.a . . . . . 6  |-  A  =  ( Base `  K
)
1614, 15syl6eqr 2333 . . . . 5  |-  ( f  =  K  ->  ( Base `  f )  =  A )
1716fveq2d 5529 . . . 4  |-  ( f  =  K  ->  (TopOn `  ( Base `  f
) )  =  (TopOn `  A ) )
1813, 17eleq12d 2351 . . 3  |-  ( f  =  K  ->  (
( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) )  <->  J  e.  (TopOn `  A ) ) )
1911, 18elab3 2921 . 2  |-  ( K  e.  { f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) ) }  <-> 
J  e.  (TopOn `  A ) )
202, 19bitri 240 1  |-  ( K  e.  TopSp 
<->  J  e.  (TopOn `  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1623    e. wcel 1684   {cab 2269   _Vcvv 2788   (/)c0 3455   ` cfv 5255   Basecbs 13148   TopOpenctopn 13326   Topctop 16631  TopOnctopon 16632   TopSpctps 16634
This theorem is referenced by:  istps2  16675  tpspropd  16678  tsettps  16681  indistps2ALT  16751  resstps  16917  prdstps  17323  imastps  17412  xpstopnlem2  17502  tmdtopon  17764  tgptopon  17765  istgp2  17774  oppgtmd  17780  distgp  17782  indistgp  17783  symgtgp  17784  divstgplem  17803  prdstmdd  17806  eltsms  17815  tsmscls  17820  tsmsgsum  17821  tsmsid  17822  tsmsmhm  17828  tsmsadd  17829  dvrcn  17866  cnmpt1vsca  17876  cnmpt2vsca  17877  tlmtgp  17878  isxms2  17994  ressxms  18071  prdsxmslem2  18075  nrgtrg  18200  cnfldtopon  18292  cnmpt1ds  18347  cnmpt2ds  18348  nmcn  18349  cnmpt1ip  18674  cnmpt2ip  18675  csscld  18676  clsocv  18677  minveclem4a  18794  mhmhmeotmd  23300
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-top 16636  df-topon 16639  df-topsp 16640
  Copyright terms: Public domain W3C validator