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

Theorem haustop 18776
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 2433 . . 3  |-  U. J  =  U. J
21ishaus 18767 . 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 457 1  |-  ( J  e.  Haus  ->  J  e. 
Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958    = wceq 1362    e. wcel 1755    =/= wne 2596   A.wral 2705   E.wrex 2706    i^i cin 3315   (/)c0 3625   U.cuni 4079   Topctop 18339   Hauscha 18753
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-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-uni 4080  df-haus 18760
This theorem is referenced by:  haust1  18797  resthaus  18813  sshaus  18820  lmmo  18825  hauscmplem  18850  hauscmp  18851  hauslly  18937  hausllycmp  18939  kgenhaus  18958  pthaus  19052  txhaus  19061  xkohaus  19067  haushmph  19206  cmphaushmeo  19214  hausflim  19395  hauspwpwf1  19401  hauspwpwdom  19402  hausflf  19411  cnextfun  19477  cnextfvval  19478  cnextf  19479  cnextcn  19480  cnextfres  19481  hausgraph  29422
  Copyright terms: Public domain W3C validator