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

Theorem toponmax 19302
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 19301 . 2  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
2 topontop 19300 . . 3  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
3 eqid 2443 . . . 4  |-  U. J  =  U. J
43topopn 19288 . . 3  |-  ( J  e.  Top  ->  U. J  e.  J )
52, 4syl 16 . 2  |-  ( J  e.  (TopOn `  B
)  ->  U. J  e.  J )
61, 5eqeltrd 2531 1  |-  ( J  e.  (TopOn `  B
)  ->  B  e.  J )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   U.cuni 4234   ` cfv 5578   Topctop 19267  TopOnctopon 19268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fv 5586  df-top 19272  df-topon 19275
This theorem is referenced by:  topgele  19308  eltpsg  19319  en2top  19360  resttopon  19535  ordtrest  19576  ordtrest2lem  19577  ordtrest2  19578  lmfval  19606  cnpfval  19608  iscn  19609  iscnp  19611  lmbrf  19634  cncls  19648  cnconst2  19657  cnrest2  19660  cndis  19665  cnindis  19666  cnpdis  19667  lmfss  19670  lmres  19674  lmff  19675  ist1-3  19723  consuba  19794  uncon  19803  kgenval  19909  elkgen  19910  kgentopon  19912  pttoponconst  19971  tx1cn  19983  tx2cn  19984  ptcls  19990  xkoccn  19993  txlm  20022  cnmpt2res  20051  xkoinjcn  20061  qtoprest  20091  ordthmeolem  20175  pt1hmeo  20180  xkocnv  20188  flimclslem  20358  flfval  20364  flfnei  20365  isflf  20367  flfcnp  20378  txflf  20380  supnfcls  20394  fclscf  20399  fclscmp  20404  fcfval  20407  isfcf  20408  uffcfflf  20413  cnpfcf  20415  mopnm  20820  isxms2  20824  prdsxmslem2  20905  bcth2  21642  dvmptid  22233  dvmptc  22234  dvtaylp  22637  taylthlem1  22640  taylthlem2  22641  pige3  22782  dvcxp1  22988  cxpcn3  22994  ordtrestNEW  27776  ordtrest2NEWlem  27777  ordtrest2NEW  27778  areacirclem1  30082  topjoin  30158
  Copyright terms: Public domain W3C validator