MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  toponmax Structured version   Unicode version

Theorem toponmax 18668
Description: The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
toponmax  |-  ( J  e.  (TopOn `  B
)  ->  B  e.  J )

Proof of Theorem toponmax
StepHypRef Expression
1 toponuni 18667 . 2  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
2 topontop 18666 . . 3  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
3 eqid 2454 . . . 4  |-  U. J  =  U. J
43topopn 18654 . . 3  |-  ( J  e.  Top  ->  U. J  e.  J )
52, 4syl 16 . 2  |-  ( J  e.  (TopOn `  B
)  ->  U. J  e.  J )
61, 5eqeltrd 2542 1  |-  ( J  e.  (TopOn `  B
)  ->  B  e.  J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   U.cuni 4202   ` cfv 5529   Topctop 18633  TopOnctopon 18634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-mpt 4463  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-iota 5492  df-fun 5531  df-fv 5537  df-top 18638  df-topon 18641
This theorem is referenced by:  topgele  18674  eltpsg  18685  en2top  18725  resttopon  18900  ordtrest  18941  ordtrest2lem  18942  ordtrest2  18943  lmfval  18971  cnpfval  18973  iscn  18974  iscnp  18976  lmbrf  18999  cncls  19013  cnconst2  19022  cnrest2  19025  cndis  19030  cnindis  19031  cnpdis  19032  lmfss  19035  lmres  19039  lmff  19040  ist1-3  19088  consuba  19159  uncon  19168  kgenval  19243  elkgen  19244  kgentopon  19246  pttoponconst  19305  tx1cn  19317  tx2cn  19318  ptcls  19324  xkoccn  19327  txlm  19356  cnmpt2res  19385  xkoinjcn  19395  qtoprest  19425  ordthmeolem  19509  pt1hmeo  19514  xkocnv  19522  flimclslem  19692  flfval  19698  flfnei  19699  isflf  19701  flfcnp  19712  txflf  19714  supnfcls  19728  fclscf  19733  fclscmp  19738  fcfval  19741  isfcf  19742  uffcfflf  19747  cnpfcf  19749  mopnm  20154  isxms2  20158  prdsxmslem2  20239  bcth2  20976  dvmptid  21567  dvmptc  21568  dvtaylp  21971  taylthlem1  21974  taylthlem2  21975  pige3  22115  dvcxp1  22316  cxpcn3  22322  ordtrestNEW  26516  ordtrest2NEWlem  26517  ordtrest2NEW  26518  areacirclem1  28652  topjoin  28754
  Copyright terms: Public domain W3C validator