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

Theorem istps 18546
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 18512 . . 3  |-  TopSp  =  {
f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f
) ) }
21eleq2i 2507 . 2  |-  ( K  e.  TopSp 
<->  K  e.  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) } )
3 topontop 18536 . . . 4  |-  ( J  e.  (TopOn `  A
)  ->  J  e.  Top )
4 0ntop 18523 . . . . . 6  |-  -.  (/)  e.  Top
5 istps.j . . . . . . . 8  |-  J  =  ( TopOpen `  K )
6 fvprc 5690 . . . . . . . 8  |-  ( -.  K  e.  _V  ->  (
TopOpen `  K )  =  (/) )
75, 6syl5eq 2487 . . . . . . 7  |-  ( -.  K  e.  _V  ->  J  =  (/) )
87eleq1d 2509 . . . . . 6  |-  ( -.  K  e.  _V  ->  ( J  e.  Top  <->  (/)  e.  Top ) )
94, 8mtbiri 303 . . . . 5  |-  ( -.  K  e.  _V  ->  -.  J  e.  Top )
109con4i 130 . . . 4  |-  ( J  e.  Top  ->  K  e.  _V )
113, 10syl 16 . . 3  |-  ( J  e.  (TopOn `  A
)  ->  K  e.  _V )
12 fveq2 5696 . . . . 5  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  ( TopOpen `  K )
)
1312, 5syl6eqr 2493 . . . 4  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  J )
14 fveq2 5696 . . . . . 6  |-  ( f  =  K  ->  ( Base `  f )  =  ( Base `  K
) )
15 istps.a . . . . . 6  |-  A  =  ( Base `  K
)
1614, 15syl6eqr 2493 . . . . 5  |-  ( f  =  K  ->  ( Base `  f )  =  A )
1716fveq2d 5700 . . . 4  |-  ( f  =  K  ->  (TopOn `  ( Base `  f
) )  =  (TopOn `  A ) )
1813, 17eleq12d 2511 . . 3  |-  ( f  =  K  ->  (
( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) )  <->  J  e.  (TopOn `  A ) ) )
1911, 18elab3 3118 . 2  |-  ( K  e.  { f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) ) }  <-> 
J  e.  (TopOn `  A ) )
202, 19bitri 249 1  |-  ( K  e.  TopSp 
<->  J  e.  (TopOn `  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    = wceq 1369    e. wcel 1756   {cab 2429   _Vcvv 2977   (/)c0 3642   ` cfv 5423   Basecbs 14179   TopOpenctopn 14365   Topctop 18503  TopOnctopon 18504   TopSpctps 18506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5386  df-fun 5425  df-fv 5431  df-top 18508  df-topon 18511  df-topsp 18512
This theorem is referenced by:  istps2  18547  tpspropd  18550  tsettps  18553  indistps2ALT  18623  resstps  18796  prdstps  19207  imastps  19299  xpstopnlem2  19389  tmdtopon  19657  tgptopon  19658  istgp2  19667  oppgtmd  19673  distgp  19675  indistgp  19676  symgtgp  19677  divstgplem  19696  prdstmdd  19699  eltsms  19708  tsmscls  19713  tsmsgsum  19714  tsmsid  19715  tsmsgsumOLD  19717  tsmsidOLD  19718  tsmsmhm  19725  tsmsadd  19726  dvrcn  19763  cnmpt1vsca  19773  cnmpt2vsca  19774  tlmtgp  19775  ressusp  19845  tustps  19853  ucncn  19865  neipcfilu  19876  cnextucn  19883  ucnextcn  19884  isxms2  20028  ressxms  20105  prdsxmslem2  20109  nrgtrg  20275  cnfldtopon  20367  cnmpt1ds  20424  cnmpt2ds  20425  nmcn  20426  cnmpt1ip  20764  cnmpt2ip  20765  csscld  20766  clsocv  20767  minveclem4a  20922  mhmhmeotmd  26362
  Copyright terms: Public domain W3C validator