Theorem topopn 18361

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 3363	. . 3 |- J C_ J
3		uniopn 18352	. . 3 |- ( ( J e. Top /\ J C_ J ) -> U. J e. J )
4	2, 3	mpan2 664	. 2 |- ( J e. Top -> U. J e. J )
5	1, 4	syl5eqel 2517	1 |- ( J e. Top -> X e. J )

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755   C_ wss 3316   U.cuni 4079   Topctop 18340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-v 2964  df-in 3323  df-ss 3330  df-pw 3850  df-uni 4080  df-top 18345

This theorem is referenced by:  riinopn  18363  istps2OLD  18368  toponmax  18375  cldval  18469  ntrfval  18470  clsfval  18471  iscld  18473  ntrval  18482  clsval  18483  0cld  18484  clsval2  18496  ntrtop  18516  toponmre  18539  neifval  18545  neif  18546  neival  18548  isnei  18549  tpnei  18567  lpfval  18584  lpval  18585  restcld  18618  restcls  18627  restntr  18628  cnrest  18731  cmpsub  18845  hauscmplem  18851  cmpfi  18853  iscon2  18860  consubclo  18870  1stcfb  18891  1stcelcls  18907  islly2  18930  lly1stc  18942  cmpkgen  18966  llycmpkgen  18967  ptbasid  18990  ptpjpre2  18995  ptopn2  18999  xkoopn  19004  xkouni  19014  txcld  19018  txcn  19041  ptrescn  19054  txtube  19055  txhaus  19062  xkoptsub  19069  xkopt  19070  xkopjcn  19071  qtoptop  19115  qtopuni  19117  opnfbas  19257  flimval  19378  flimfil  19384  hausflim  19396  hauspwpwf1  19402  hauspwpwdom  19403  flimfnfcls  19443  cnpfcfi  19455  bcthlem5  20681  dvply1  21635  cldssbrsiga  26455  dya2iocucvr  26553  kur14lem7  26948  kur14lem9  26950  conpcon  26972  cvmliftmolem1  27018  ordtop  28130  islocfin  28412  finlocfin  28415