Theorem topopn 20711

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 3624	. . 3 |- J C_ J
3		uniopn 20702	. . 3 |- ( ( J e. Top /\ J C_ J ) -> U. J e. J )
4	2, 3	mpan2 707	. 2 |- ( J e. Top -> U. J e. J )
5	1, 4	syl5eqel 2705	1 |- ( J e. Top -> X e. J )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   C_ wss 3574   U.cuni 4436   Topctop 20698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160  df-uni 4437  df-top 20699

This theorem is referenced by:  riinopn  20713  toponmax  20730  cldval  20827  ntrfval  20828  clsfval  20829  iscld  20831  ntrval  20840  clsval  20841  0cld  20842  clsval2  20854  ntrtop  20874  toponmre  20897  neifval  20903  neif  20904  neival  20906  isnei  20907  tpnei  20925  lpfval  20942  lpval  20943  restcld  20976  restcls  20985  restntr  20986  cnrest  21089  cmpsub  21203  hauscmplem  21209  cmpfi  21211  isconn2  21217  connsubclo  21227  1stcfb  21248  1stcelcls  21264  islly2  21287  lly1stc  21299  islocfin  21320  finlocfin  21323  cmpkgen  21354  llycmpkgen  21355  ptbasid  21378  ptpjpre2  21383  ptopn2  21387  xkoopn  21392  xkouni  21402  txcld  21406  txcn  21429  ptrescn  21442  txtube  21443  txhaus  21450  xkoptsub  21457  xkopt  21458  xkopjcn  21459  qtoptop  21503  qtopuni  21505  opnfbas  21646  flimval  21767  flimfil  21773  hausflim  21785  hauspwpwf1  21791  hauspwpwdom  21792  flimfnfcls  21832  cnpfcfi  21844  bcthlem5  23125  dvply1  24039  cldssbrsiga  30250  dya2iocucvr  30346  kur14lem7  31194  kur14lem9  31196  connpconn  31217  cvmliftmolem1  31263  ordtop  32435  ntrelmap  38423  clselmap  38425  dssmapntrcls  38426  dssmapclsntr  38427  reopn  39501