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

Theorem topopn 19984
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 3462 . . 3  |-  J  C_  J
3 uniopn 19975 . . 3  |-  ( ( J  e.  Top  /\  J  C_  J )  ->  U. J  e.  J
)
42, 3mpan2 682 . 2  |-  ( J  e.  Top  ->  U. J  e.  J )
51, 4syl5eqel 2543 1  |-  ( J  e.  Top  ->  X  e.  J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454    e. wcel 1897    C_ wss 3415   U.cuni 4211   Topctop 19965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-rex 2754  df-v 3058  df-in 3422  df-ss 3429  df-pw 3964  df-uni 4212  df-top 19969
This theorem is referenced by:  riinopn  19986  toponmax  19991  cldval  20086  ntrfval  20087  clsfval  20088  iscld  20090  ntrval  20099  clsval  20100  0cld  20101  clsval2  20113  ntrtop  20134  toponmre  20157  neifval  20163  neif  20164  neival  20166  isnei  20167  tpnei  20185  lpfval  20202  lpval  20203  restcld  20236  restcls  20245  restntr  20246  cnrest  20349  cmpsub  20463  hauscmplem  20469  cmpfi  20471  iscon2  20477  consubclo  20487  1stcfb  20508  1stcelcls  20524  islly2  20547  lly1stc  20559  islocfin  20580  finlocfin  20583  cmpkgen  20614  llycmpkgen  20615  ptbasid  20638  ptpjpre2  20643  ptopn2  20647  xkoopn  20652  xkouni  20662  txcld  20666  txcn  20689  ptrescn  20702  txtube  20703  txhaus  20710  xkoptsub  20717  xkopt  20718  xkopjcn  20719  qtoptop  20763  qtopuni  20765  opnfbas  20905  flimval  21026  flimfil  21032  hausflim  21044  hauspwpwf1  21050  hauspwpwdom  21051  flimfnfcls  21091  cnpfcfi  21103  bcthlem5  22344  dvply1  23285  cldssbrsiga  29057  dya2iocucvr  29154  kur14lem7  29983  kur14lem9  29985  conpcon  30006  cvmliftmolem1  30052  ordtop  31144  reopn  37539
  Copyright terms: Public domain W3C validator