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

Theorem topopn 20639
Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
Hypothesis
Ref Expression
1open.1 𝑋 = 𝐽
Assertion
Ref Expression
topopn (𝐽 ∈ Top → 𝑋𝐽)

Proof of Theorem topopn
StepHypRef Expression
1 1open.1 . 2 𝑋 = 𝐽
2 ssid 3608 . . 3 𝐽𝐽
3 uniopn 20630 . . 3 ((𝐽 ∈ Top ∧ 𝐽𝐽) → 𝐽𝐽)
42, 3mpan2 706 . 2 (𝐽 ∈ Top → 𝐽𝐽)
51, 4syl5eqel 2702 1 (𝐽 ∈ Top → 𝑋𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  wss 3559   cuni 4407  Topctop 20626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3191  df-in 3566  df-ss 3573  df-pw 4137  df-uni 4408  df-top 20627
This theorem is referenced by:  riinopn  20641  toponmax  20648  cldval  20746  ntrfval  20747  clsfval  20748  iscld  20750  ntrval  20759  clsval  20760  0cld  20761  clsval2  20773  ntrtop  20793  toponmre  20816  neifval  20822  neif  20823  neival  20825  isnei  20826  tpnei  20844  lpfval  20861  lpval  20862  restcld  20895  restcls  20904  restntr  20905  cnrest  21008  cmpsub  21122  hauscmplem  21128  cmpfi  21130  isconn2  21136  connsubclo  21146  1stcfb  21167  1stcelcls  21183  islly2  21206  lly1stc  21218  islocfin  21239  finlocfin  21242  cmpkgen  21273  llycmpkgen  21274  ptbasid  21297  ptpjpre2  21302  ptopn2  21306  xkoopn  21311  xkouni  21321  txcld  21325  txcn  21348  ptrescn  21361  txtube  21362  txhaus  21369  xkoptsub  21376  xkopt  21377  xkopjcn  21378  qtoptop  21422  qtopuni  21424  opnfbas  21565  flimval  21686  flimfil  21692  hausflim  21704  hauspwpwf1  21710  hauspwpwdom  21711  flimfnfcls  21751  cnpfcfi  21763  bcthlem5  23044  dvply1  23956  cldssbrsiga  30049  dya2iocucvr  30145  kur14lem7  30929  kur14lem9  30931  connpconn  30952  cvmliftmolem1  30998  ordtop  32104  ntrelmap  37932  clselmap  37934  dssmapntrcls  37935  dssmapclsntr  37936  reopn  38988
  Copyright terms: Public domain W3C validator