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

Theorem haustop 20127
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 2404 . . 3  |-  U. J  =  U. J
21ishaus 20118 . 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 976    = wceq 1407    e. wcel 1844    =/= wne 2600   A.wral 2756   E.wrex 2757    i^i cin 3415   (/)c0 3740   U.cuni 4193   Topctop 19688   Hauscha 20104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-uni 4194  df-haus 20111
This theorem is referenced by:  haust1  20148  resthaus  20164  sshaus  20171  lmmo  20176  hauscmplem  20201  hauscmp  20202  hauslly  20287  hausllycmp  20289  kgenhaus  20339  pthaus  20433  txhaus  20442  xkohaus  20448  haushmph  20587  cmphaushmeo  20595  hausflim  20776  hauspwpwf1  20782  hauspwpwdom  20783  hausflf  20792  cnextfun  20858  cnextfvval  20859  cnextf  20860  cnextcn  20861  cnextfres  20862  qtophaus  28305  ismntop  28469  hausgraph  35549
  Copyright terms: Public domain W3C validator