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

Theorem haustop 22705
Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.)
Assertion
Ref Expression
haustop (𝐽 ∈ Haus → 𝐽 ∈ Top)

Proof of Theorem haustop
Dummy variables 𝑥 𝑦 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2733 . . 3 𝐽 = 𝐽
21ishaus 22696 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑛𝐽𝑚𝐽 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))))
32simplbi 499 1 (𝐽 ∈ Haus → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088   = wceq 1542  wcel 2107  wne 2940  wral 3061  wrex 3070  cin 3913  c0 4286   cuni 4869  Topctop 22265  Hauscha 22682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-in 3921  df-ss 3931  df-uni 4870  df-haus 22689
This theorem is referenced by:  haust1  22726  resthaus  22742  sshaus  22749  lmmo  22754  hauscmplem  22780  hauscmp  22781  hauslly  22866  hausllycmp  22868  kgenhaus  22918  pthaus  23012  txhaus  23021  xkohaus  23027  haushmph  23166  cmphaushmeo  23174  hausflim  23355  hauspwpwf1  23361  hauspwpwdom  23362  hausflf  23371  cnextfun  23438  cnextfvval  23439  cnextf  23440  cnextcn  23441  cnextfres1  23442  cnextfres  23443  qtophaus  32481  ismntop  32671  poimirlem30  36158  hausgraph  41586
  Copyright terms: Public domain W3C validator