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

Theorem toponmax 18508
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 18507 . 2  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
2 topontop 18506 . . 3  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
3 eqid 2438 . . . 4  |-  U. J  =  U. J
43topopn 18494 . . 3  |-  ( J  e.  Top  ->  U. J  e.  J )
52, 4syl 16 . 2  |-  ( J  e.  (TopOn `  B
)  ->  U. J  e.  J )
61, 5eqeltrd 2512 1  |-  ( J  e.  (TopOn `  B
)  ->  B  e.  J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   U.cuni 4086   ` cfv 5413   Topctop 18473  TopOnctopon 18474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fv 5421  df-top 18478  df-topon 18481
This theorem is referenced by:  topgele  18514  eltpsg  18525  en2top  18565  resttopon  18740  ordtrest  18781  ordtrest2lem  18782  ordtrest2  18783  lmfval  18811  cnpfval  18813  iscn  18814  iscnp  18816  lmbrf  18839  cncls  18853  cnconst2  18862  cnrest2  18865  cndis  18870  cnindis  18871  cnpdis  18872  lmfss  18875  lmres  18879  lmff  18880  ist1-3  18928  consuba  18999  uncon  19008  kgenval  19083  elkgen  19084  kgentopon  19086  pttoponconst  19145  tx1cn  19157  tx2cn  19158  ptcls  19164  xkoccn  19167  txlm  19196  cnmpt2res  19225  xkoinjcn  19235  qtoprest  19265  ordthmeolem  19349  pt1hmeo  19354  xkocnv  19362  flimclslem  19532  flfval  19538  flfnei  19539  isflf  19541  flfcnp  19552  txflf  19554  supnfcls  19568  fclscf  19573  fclscmp  19578  fcfval  19581  isfcf  19582  uffcfflf  19587  cnpfcf  19589  mopnm  19994  isxms2  19998  prdsxmslem2  20079  bcth2  20816  dvmptid  21406  dvmptc  21407  dvtaylp  21810  taylthlem1  21813  taylthlem2  21814  pige3  21954  dvcxp1  22155  cxpcn3  22161  ordtrestNEW  26303  ordtrest2NEWlem  26304  ordtrest2NEW  26305  areacirclem1  28437  topjoin  28539
  Copyright terms: Public domain W3C validator