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

Theorem topopn 16668
Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
Hypothesis
Ref Expression
1open.1  |-  X  = 
U. J
Assertion
Ref Expression
topopn  |-  ( J  e.  Top  ->  X  e.  J )

Proof of Theorem topopn
StepHypRef Expression
1 1open.1 . 2  |-  X  = 
U. J
2 ssid 3210 . . 3  |-  J  C_  J
3 uniopn 16659 . . 3  |-  ( ( J  e.  Top  /\  J  C_  J )  ->  U. J  e.  J
)
42, 3mpan2 652 . 2  |-  ( J  e.  Top  ->  U. J  e.  J )
51, 4syl5eqel 2380 1  |-  ( J  e.  Top  ->  X  e.  J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696    C_ wss 3165   U.cuni 3843   Topctop 16647
This theorem is referenced by:  riinopn  16670  istps2OLD  16675  toponmax  16682  cldval  16776  ntrfval  16777  clsfval  16778  iscld  16780  ntrval  16789  clsval  16790  0cld  16791  clsval2  16803  ntrtop  16823  toponmre  16846  neifval  16852  neif  16853  neival  16855  isnei  16856  tpnei  16874  lpfval  16886  lpval  16887  restcld  16919  restcls  16927  restntr  16928  cnrest  17029  cmpsub  17143  hauscmplem  17149  cmpfi  17151  iscon2  17156  consubclo  17166  1stcfb  17187  1stcelcls  17203  islly2  17226  lly1stc  17238  cmpkgen  17262  llycmpkgen  17263  ptbasid  17286  ptpjpre2  17291  ptopn2  17295  xkoopn  17300  xkouni  17310  txcld  17314  txcn  17336  ptrescn  17349  txtube  17350  txhaus  17357  xkoptsub  17364  xkopt  17365  xkopjcn  17366  qtoptop  17407  qtopuni  17409  opnfbas  17553  flimval  17674  flimfil  17680  hausflim  17692  hauspwpwf1  17698  hauspwpwdom  17699  flimfnfcls  17739  cnpfcfi  17751  bcthlem5  18766  dvply1  19680  cldssbrsiga  23533  kur14lem7  23758  kur14lem9  23760  conpcon  23781  cvmliftmolem1  23827  ordtop  24947  unint2t  25621  intfmu2  25622  mapdiscn  25630  mapudiscn  25631  intopcoaconlem3b  25641  intopcoaconlem3  25642  cnpflf4  25667  islimrs4  25685  islocfin  26399  finlocfin  26402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640  df-uni 3844  df-top 16652
  Copyright terms: Public domain W3C validator