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

Theorem topopn 16984
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 3369 . . 3  |-  J  C_  J
3 uniopn 16975 . . 3  |-  ( ( J  e.  Top  /\  J  C_  J )  ->  U. J  e.  J
)
42, 3mpan2 654 . 2  |-  ( J  e.  Top  ->  U. J  e.  J )
51, 4syl5eqel 2522 1  |-  ( J  e.  Top  ->  X  e.  J )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726    C_ wss 3322   U.cuni 4017   Topctop 16963
This theorem is referenced by:  riinopn  16986  istps2OLD  16991  toponmax  16998  cldval  17092  ntrfval  17093  clsfval  17094  iscld  17096  ntrval  17105  clsval  17106  0cld  17107  clsval2  17119  ntrtop  17139  toponmre  17162  neifval  17168  neif  17169  neival  17171  isnei  17172  tpnei  17190  lpfval  17207  lpval  17208  restcld  17241  restcls  17250  restntr  17251  cnrest  17354  cmpsub  17468  hauscmplem  17474  cmpfi  17476  iscon2  17482  consubclo  17492  1stcfb  17513  1stcelcls  17529  islly2  17552  lly1stc  17564  cmpkgen  17588  llycmpkgen  17589  ptbasid  17612  ptpjpre2  17617  ptopn2  17621  xkoopn  17626  xkouni  17636  txcld  17640  txcn  17663  ptrescn  17676  txtube  17677  txhaus  17684  xkoptsub  17691  xkopt  17692  xkopjcn  17693  qtoptop  17737  qtopuni  17739  opnfbas  17879  flimval  18000  flimfil  18006  hausflim  18018  hauspwpwf1  18024  hauspwpwdom  18025  flimfnfcls  18065  cnpfcfi  18077  bcthlem5  19286  dvply1  20206  cldssbrsiga  24546  dya2iocucvr  24639  kur14lem7  24903  kur14lem9  24905  conpcon  24927  cvmliftmolem1  24973  ordtop  26191  islocfin  26390  finlocfin  26393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-in 3329  df-ss 3336  df-pw 3803  df-uni 4018  df-top 16968
  Copyright terms: Public domain W3C validator