Theorem topopn 19182

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 3523	. . 3 |- J C_ J
3		uniopn 19173	. . 3 |- ( ( J e. Top /\ J C_ J ) -> U. J e. J )
4	2, 3	mpan2 671	. 2 |- ( J e. Top -> U. J e. J )
5	1, 4	syl5eqel 2559	1 |- ( J e. Top -> X e. J )

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   C_ wss 3476   U.cuni 4245   Topctop 19161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012  df-uni 4246  df-top 19166

This theorem is referenced by:  riinopn  19184  istps2OLD  19189  toponmax  19196  cldval  19290  ntrfval  19291  clsfval  19292  iscld  19294  ntrval  19303  clsval  19304  0cld  19305  clsval2  19317  ntrtop  19337  toponmre  19360  neifval  19366  neif  19367  neival  19369  isnei  19370  tpnei  19388  lpfval  19405  lpval  19406  restcld  19439  restcls  19448  restntr  19449  cnrest  19552  cmpsub  19666  hauscmplem  19672  cmpfi  19674  iscon2  19681  consubclo  19691  1stcfb  19712  1stcelcls  19728  islly2  19751  lly1stc  19763  cmpkgen  19787  llycmpkgen  19788  ptbasid  19811  ptpjpre2  19816  ptopn2  19820  xkoopn  19825  xkouni  19835  txcld  19839  txcn  19862  ptrescn  19875  txtube  19876  txhaus  19883  xkoptsub  19890  xkopt  19891  xkopjcn  19892  qtoptop  19936  qtopuni  19938  opnfbas  20078  flimval  20199  flimfil  20205  hausflim  20217  hauspwpwf1  20223  hauspwpwdom  20224  flimfnfcls  20264  cnpfcfi  20276  bcthlem5  21502  dvply1  22414  cldssbrsiga  27798  dya2iocucvr  27895  kur14lem7  28296  kur14lem9  28298  conpcon  28320  cvmliftmolem1  28366  ordtop  29478  islocfin  29768  finlocfin  29771  reopn  31053  dirkeritg  31402