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

Theorem topopn 21490
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 3968 . . 3 𝐽𝐽
3 uniopn 21481 . . 3 ((𝐽 ∈ Top ∧ 𝐽𝐽) → 𝐽𝐽)
42, 3mpan2 689 . 2 (𝐽 ∈ Top → 𝐽𝐽)
51, 4eqeltrid 2915 1 (𝐽 ∈ Top → 𝑋𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2114  wss 3913   cuni 4814  Topctop 21477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rab 3134  df-v 3475  df-in 3920  df-ss 3930  df-pw 4517  df-uni 4815  df-top 21478
This theorem is referenced by:  riinopn  21492  toponmax  21510  cldval  21607  ntrfval  21608  clsfval  21609  iscld  21611  ntrval  21620  clsval  21621  0cld  21622  clsval2  21634  ntrtop  21654  toponmre  21677  neifval  21683  neif  21684  neival  21686  isnei  21687  tpnei  21705  lpfval  21722  lpval  21723  restcld  21756  restcls  21765  restntr  21766  cnrest  21869  cmpsub  21984  hauscmplem  21990  cmpfi  21992  isconn2  21998  connsubclo  22008  1stcfb  22029  1stcelcls  22045  islly2  22068  lly1stc  22080  islocfin  22101  finlocfin  22104  cmpkgen  22135  llycmpkgen  22136  ptbasid  22159  ptpjpre2  22164  ptopn2  22168  xkoopn  22173  xkouni  22183  txcld  22187  txcn  22210  ptrescn  22223  txtube  22224  txhaus  22231  xkoptsub  22238  xkopt  22239  xkopjcn  22240  qtoptop  22284  qtopuni  22286  opnfbas  22426  flimval  22547  flimfil  22553  hausflim  22565  hauspwpwf1  22571  hauspwpwdom  22572  flimfnfcls  22612  cnpfcfi  22624  bcthlem5  23911  dvply1  24859  cldssbrsiga  31454  dya2iocucvr  31550  kur14lem7  32467  kur14lem9  32469  connpconn  32490  cvmliftmolem1  32536  ordtop  33792  pibt2  34715  ntrelmap  40610  clselmap  40612  dssmapntrcls  40613  dssmapclsntr  40614  reopn  41709
  Copyright terms: Public domain W3C validator