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

Theorem haustop 19598
Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.)
Assertion
Ref Expression
haustop  |-  ( J  e.  Haus  ->  J  e. 
Top )

Proof of Theorem haustop
Dummy variables  x  y  m  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . . 3  |-  U. J  =  U. J
21ishaus 19589 . 2  |-  ( J  e.  Haus  <->  ( J  e. 
Top  /\  A. x  e.  U. J A. y  e.  U. J ( x  =/=  y  ->  E. n  e.  J  E. m  e.  J  ( x  e.  n  /\  y  e.  m  /\  (
n  i^i  m )  =  (/) ) ) ) )
32simplbi 460 1  |-  ( J  e.  Haus  ->  J  e. 
Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2814   E.wrex 2815    i^i cin 3475   (/)c0 3785   U.cuni 4245   Topctop 19161   Hauscha 19575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-uni 4246  df-haus 19582
This theorem is referenced by:  haust1  19619  resthaus  19635  sshaus  19642  lmmo  19647  hauscmplem  19672  hauscmp  19673  hauslly  19759  hausllycmp  19761  kgenhaus  19780  pthaus  19874  txhaus  19883  xkohaus  19889  haushmph  20028  cmphaushmeo  20036  hausflim  20217  hauspwpwf1  20223  hauspwpwdom  20224  hausflf  20233  cnextfun  20299  cnextfvval  20300  cnextf  20301  cnextcn  20302  cnextfres  20303  qtophaus  27637  ismntop  27644  hausgraph  30777
  Copyright terms: Public domain W3C validator