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

Theorem haustop 18940
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 2443 . . 3  |-  U. J  =  U. J
21ishaus 18931 . 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 965    = wceq 1369    e. wcel 1756    =/= wne 2611   A.wral 2720   E.wrex 2721    i^i cin 3332   (/)c0 3642   U.cuni 4096   Topctop 18503   Hauscha 18917
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-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-uni 4097  df-haus 18924
This theorem is referenced by:  haust1  18961  resthaus  18977  sshaus  18984  lmmo  18989  hauscmplem  19014  hauscmp  19015  hauslly  19101  hausllycmp  19103  kgenhaus  19122  pthaus  19216  txhaus  19225  xkohaus  19231  haushmph  19370  cmphaushmeo  19378  hausflim  19559  hauspwpwf1  19565  hauspwpwdom  19566  hausflf  19575  cnextfun  19641  cnextfvval  19642  cnextf  19643  cnextcn  19644  cnextfres  19645  hausgraph  29585
  Copyright terms: Public domain W3C validator