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

Theorem toponmax 18374
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 18373 . 2  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
2 topontop 18372 . . 3  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
3 eqid 2433 . . . 4  |-  U. J  =  U. J
43topopn 18360 . . 3  |-  ( J  e.  Top  ->  U. J  e.  J )
52, 4syl 16 . 2  |-  ( J  e.  (TopOn `  B
)  ->  U. J  e.  J )
61, 5eqeltrd 2507 1  |-  ( J  e.  (TopOn `  B
)  ->  B  e.  J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   U.cuni 4079   ` cfv 5406   Topctop 18339  TopOnctopon 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-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-iota 5369  df-fun 5408  df-fv 5414  df-top 18344  df-topon 18347
This theorem is referenced by:  topgele  18380  eltpsg  18391  en2top  18431  resttopon  18606  ordtrest  18647  ordtrest2lem  18648  ordtrest2  18649  lmfval  18677  cnpfval  18679  iscn  18680  iscnp  18682  lmbrf  18705  cncls  18719  cnconst2  18728  cnrest2  18731  cndis  18736  cnindis  18737  cnpdis  18738  lmfss  18741  lmres  18745  lmff  18746  ist1-3  18794  consuba  18865  uncon  18874  kgenval  18949  elkgen  18950  kgentopon  18952  pttoponconst  19011  tx1cn  19023  tx2cn  19024  ptcls  19030  xkoccn  19033  txlm  19062  cnmpt2res  19091  xkoinjcn  19101  qtoprest  19131  ordthmeolem  19215  pt1hmeo  19220  xkocnv  19228  flimclslem  19398  flfval  19404  flfnei  19405  isflf  19407  flfcnp  19418  txflf  19420  supnfcls  19434  fclscf  19439  fclscmp  19444  fcfval  19447  isfcf  19448  uffcfflf  19453  cnpfcf  19455  mopnm  19860  isxms2  19864  prdsxmslem2  19945  bcth2  20682  dvmptid  21272  dvmptc  21273  dvtaylp  21719  taylthlem1  21722  taylthlem2  21723  pige3  21863  dvcxp1  22064  cxpcn3  22070  ordtrestNEW  26204  ordtrest2NEWlem  26205  ordtrest2NEW  26206  areacirclem1  28325  topjoin  28427
  Copyright terms: Public domain W3C validator