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

Theorem topopn 16652
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 3197 . . 3  |-  J  C_  J
3 uniopn 16643 . . 3  |-  ( ( J  e.  Top  /\  J  C_  J )  ->  U. J  e.  J
)
42, 3mpan2 652 . 2  |-  ( J  e.  Top  ->  U. J  e.  J )
51, 4syl5eqel 2367 1  |-  ( J  e.  Top  ->  X  e.  J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684    C_ wss 3152   U.cuni 3827   Topctop 16631
This theorem is referenced by:  riinopn  16654  istps2OLD  16659  toponmax  16666  cldval  16760  ntrfval  16761  clsfval  16762  iscld  16764  ntrval  16773  clsval  16774  0cld  16775  clsval2  16787  ntrtop  16807  toponmre  16830  neifval  16836  neif  16837  neival  16839  isnei  16840  tpnei  16858  lpfval  16870  lpval  16871  restcld  16903  restcls  16911  restntr  16912  cnrest  17013  cmpsub  17127  hauscmplem  17133  cmpfi  17135  iscon2  17140  consubclo  17150  1stcfb  17171  1stcelcls  17187  islly2  17210  lly1stc  17222  cmpkgen  17246  llycmpkgen  17247  ptbasid  17270  ptpjpre2  17275  ptopn2  17279  xkoopn  17284  xkouni  17294  txcld  17298  txcn  17320  ptrescn  17333  txtube  17334  txhaus  17341  xkoptsub  17348  xkopt  17349  xkopjcn  17350  qtoptop  17391  qtopuni  17393  opnfbas  17537  flimval  17658  flimfil  17664  hausflim  17676  hauspwpwf1  17682  hauspwpwdom  17683  flimfnfcls  17723  cnpfcfi  17735  bcthlem5  18750  dvply1  19664  cldssbrsiga  23518  kur14lem7  23743  kur14lem9  23745  conpcon  23766  cvmliftmolem1  23812  ordtop  24875  unint2t  25518  intfmu2  25519  mapdiscn  25527  mapudiscn  25528  intopcoaconlem3b  25538  intopcoaconlem3  25539  cnpflf4  25564  islimrs4  25582  islocfin  26296  finlocfin  26299
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-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627  df-uni 3828  df-top 16636
  Copyright terms: Public domain W3C validator