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

Theorem topopn 16942
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 3335 . . 3  |-  J  C_  J
3 uniopn 16933 . . 3  |-  ( ( J  e.  Top  /\  J  C_  J )  ->  U. J  e.  J
)
42, 3mpan2 653 . 2  |-  ( J  e.  Top  ->  U. J  e.  J )
51, 4syl5eqel 2496 1  |-  ( J  e.  Top  ->  X  e.  J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721    C_ wss 3288   U.cuni 3983   Topctop 16921
This theorem is referenced by:  riinopn  16944  istps2OLD  16949  toponmax  16956  cldval  17050  ntrfval  17051  clsfval  17052  iscld  17054  ntrval  17063  clsval  17064  0cld  17065  clsval2  17077  ntrtop  17097  toponmre  17120  neifval  17126  neif  17127  neival  17129  isnei  17130  tpnei  17148  lpfval  17165  lpval  17166  restcld  17198  restcls  17207  restntr  17208  cnrest  17311  cmpsub  17425  hauscmplem  17431  cmpfi  17433  iscon2  17438  consubclo  17448  1stcfb  17469  1stcelcls  17485  islly2  17508  lly1stc  17520  cmpkgen  17544  llycmpkgen  17545  ptbasid  17568  ptpjpre2  17573  ptopn2  17577  xkoopn  17582  xkouni  17592  txcld  17596  txcn  17619  ptrescn  17632  txtube  17633  txhaus  17640  xkoptsub  17647  xkopt  17648  xkopjcn  17649  qtoptop  17693  qtopuni  17695  opnfbas  17835  flimval  17956  flimfil  17962  hausflim  17974  hauspwpwf1  17980  hauspwpwdom  17981  flimfnfcls  18021  cnpfcfi  18033  bcthlem5  19242  dvply1  20162  cldssbrsiga  24502  dya2iocucvr  24595  kur14lem7  24859  kur14lem9  24861  conpcon  24883  cvmliftmolem1  24929  ordtop  26098  islocfin  26274  finlocfin  26277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-rex 2680  df-v 2926  df-in 3295  df-ss 3302  df-pw 3769  df-uni 3984  df-top 16926
  Copyright terms: Public domain W3C validator