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

Theorem istps 19729
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 19695 . . 3  |-  TopSp  =  {
f  |  ( TopOpen `  f )  e.  (TopOn `  ( Base `  f
) ) }
21eleq2i 2480 . 2  |-  ( K  e.  TopSp 
<->  K  e.  { f  |  ( TopOpen `  f
)  e.  (TopOn `  ( Base `  f )
) } )
3 topontop 19719 . . . 4  |-  ( J  e.  (TopOn `  A
)  ->  J  e.  Top )
4 0ntop 19706 . . . . . 6  |-  -.  (/)  e.  Top
5 istps.j . . . . . . . 8  |-  J  =  ( TopOpen `  K )
6 fvprc 5843 . . . . . . . 8  |-  ( -.  K  e.  _V  ->  (
TopOpen `  K )  =  (/) )
75, 6syl5eq 2455 . . . . . . 7  |-  ( -.  K  e.  _V  ->  J  =  (/) )
87eleq1d 2471 . . . . . 6  |-  ( -.  K  e.  _V  ->  ( J  e.  Top  <->  (/)  e.  Top ) )
94, 8mtbiri 301 . . . . 5  |-  ( -.  K  e.  _V  ->  -.  J  e.  Top )
109con4i 130 . . . 4  |-  ( J  e.  Top  ->  K  e.  _V )
113, 10syl 17 . . 3  |-  ( J  e.  (TopOn `  A
)  ->  K  e.  _V )
12 fveq2 5849 . . . . 5  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  ( TopOpen `  K )
)
1312, 5syl6eqr 2461 . . . 4  |-  ( f  =  K  ->  ( TopOpen
`  f )  =  J )
14 fveq2 5849 . . . . . 6  |-  ( f  =  K  ->  ( Base `  f )  =  ( Base `  K
) )
15 istps.a . . . . . 6  |-  A  =  ( Base `  K
)
1614, 15syl6eqr 2461 . . . . 5  |-  ( f  =  K  ->  ( Base `  f )  =  A )
1716fveq2d 5853 . . . 4  |-  ( f  =  K  ->  (TopOn `  ( Base `  f
) )  =  (TopOn `  A ) )
1813, 17eleq12d 2484 . . 3  |-  ( f  =  K  ->  (
( TopOpen `  f )  e.  (TopOn `  ( Base `  f ) )  <->  J  e.  (TopOn `  A ) ) )
1911, 18elab3 3203 . 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 1405    e. wcel 1842   {cab 2387   _Vcvv 3059   (/)c0 3738   ` cfv 5569   Basecbs 14841   TopOpenctopn 15036   Topctop 19686  TopOnctopon 19687   TopSpctps 19689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-iota 5533  df-fun 5571  df-fv 5577  df-top 19691  df-topon 19694  df-topsp 19695
This theorem is referenced by:  istps2  19730  tpspropd  19733  tsettps  19736  indistps2ALT  19807  resstps  19981  prdstps  20422  imastps  20514  xpstopnlem2  20604  tmdtopon  20872  tgptopon  20873  istgp2  20882  oppgtmd  20888  distgp  20890  indistgp  20891  symgtgp  20892  qustgplem  20911  prdstmdd  20914  eltsms  20923  tsmscls  20928  tsmsgsum  20929  tsmsid  20930  tsmsgsumOLD  20932  tsmsidOLD  20933  tsmsmhm  20940  tsmsadd  20941  dvrcn  20978  cnmpt1vsca  20988  cnmpt2vsca  20989  tlmtgp  20990  ressusp  21060  tustps  21068  ucncn  21080  neipcfilu  21091  cnextucn  21098  ucnextcn  21099  isxms2  21243  ressxms  21320  prdsxmslem2  21324  nrgtrg  21490  cnfldtopon  21582  cnmpt1ds  21639  cnmpt2ds  21640  nmcn  21641  cnmpt1ip  21979  cnmpt2ip  21980  csscld  21981  clsocv  21982  minveclem4a  22137  mhmhmeotmd  28362
  Copyright terms: Public domain W3C validator