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

Theorem istps 20006
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 19979 . . 3  |-  TopSp  =  {
f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f
) ) }
21eleq2i 2532 . 2  |-  ( K  e.  TopSp 
<->  K  e.  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) } )
3 topontop 19996 . . . 4  |-  ( J  e.  (TopOn `  A
)  ->  J  e.  Top )
4 0ntop 19990 . . . . . 6  |-  -.  (/)  e.  Top
5 istps.j . . . . . . . 8  |-  J  =  ( TopOpen `  K )
6 fvprc 5886 . . . . . . . 8  |-  ( -.  K  e.  _V  ->  (
TopOpen `  K )  =  (/) )
75, 6syl5eq 2508 . . . . . . 7  |-  ( -.  K  e.  _V  ->  J  =  (/) )
87eleq1d 2524 . . . . . 6  |-  ( -.  K  e.  _V  ->  ( J  e.  Top  <->  (/)  e.  Top ) )
94, 8mtbiri 309 . . . . 5  |-  ( -.  K  e.  _V  ->  -.  J  e.  Top )
109con4i 135 . . . 4  |-  ( J  e.  Top  ->  K  e.  _V )
113, 10syl 17 . . 3  |-  ( J  e.  (TopOn `  A
)  ->  K  e.  _V )
12 fveq2 5892 . . . . 5  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  ( TopOpen `  K )
)
1312, 5syl6eqr 2514 . . . 4  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  J )
14 fveq2 5892 . . . . . 6  |-  ( f  =  K  ->  ( Base `  f )  =  ( Base `  K
) )
15 istps.a . . . . . 6  |-  A  =  ( Base `  K
)
1614, 15syl6eqr 2514 . . . . 5  |-  ( f  =  K  ->  ( Base `  f )  =  A )
1716fveq2d 5896 . . . 4  |-  ( f  =  K  ->  (TopOn `  ( Base `  f
) )  =  (TopOn `  A ) )
1813, 17eleq12d 2534 . . 3  |-  ( f  =  K  ->  (
( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) )  <->  J  e.  (TopOn `  A ) ) )
1911, 18elab3 3204 . 2  |-  ( K  e.  { f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) ) }  <-> 
J  e.  (TopOn `  A ) )
202, 19bitri 257 1  |-  ( K  e.  TopSp 
<->  J  e.  (TopOn `  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189    = wceq 1455    e. wcel 1898   {cab 2448   _Vcvv 3057   (/)c0 3743   ` cfv 5605   Basecbs 15176   TopOpenctopn 15375   Topctop 19972  TopOnctopon 19973   TopSpctps 19974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-iota 5569  df-fun 5607  df-fv 5613  df-top 19976  df-topon 19978  df-topsp 19979
This theorem is referenced by:  istps2  20007  tpspropd  20010  tsettps  20013  indistps2ALT  20084  resstps  20258  prdstps  20699  imastps  20791  xpstopnlem2  20881  tmdtopon  21151  tgptopon  21152  istgp2  21161  oppgtmd  21167  distgp  21169  indistgp  21170  symgtgp  21171  qustgplem  21190  prdstmdd  21193  eltsms  21202  tsmscls  21207  tsmsgsum  21208  tsmsid  21209  tsmsmhm  21215  tsmsadd  21216  dvrcn  21253  cnmpt1vsca  21263  cnmpt2vsca  21264  tlmtgp  21265  ressusp  21335  tustps  21343  ucncn  21355  neipcfilu  21366  cnextucn  21373  ucnextcn  21374  isxms2  21518  ressxms  21595  prdsxmslem2  21599  nrgtrg  21747  cnfldtopon  21858  cnmpt1ds  21915  cnmpt2ds  21916  nmcn  21917  cnmpt1ip  22273  cnmpt2ip  22274  csscld  22275  clsocv  22276  minveclem4a  22427  minveclem4aOLD  22439  mhmhmeotmd  28784  rrxtopon  38258  qndenserrnopnlem  38267
  Copyright terms: Public domain W3C validator