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

Step	Hyp	Ref	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 )
4	2, 3	mpan2 682	. 2 |- ( J e. Top -> U. J e. J )
5	1, 4	syl5eqel 2543	1 |- ( J e. Top -> X e. J )

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