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

Theorem haustop 21867
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 2818 . . 3 𝐽 = 𝐽
21ishaus 21858 . 2 (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 𝐽𝑦 𝐽(𝑥𝑦 → ∃𝑛𝐽𝑚𝐽 (𝑥𝑛𝑦𝑚 ∧ (𝑛𝑚) = ∅))))
32simplbi 498 1 (𝐽 ∈ Haus → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  cin 3932  c0 4288   cuni 4830  Topctop 21429  Hauscha 21844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-uni 4831  df-haus 21851
This theorem is referenced by:  haust1  21888  resthaus  21904  sshaus  21911  lmmo  21916  hauscmplem  21942  hauscmp  21943  hauslly  22028  hausllycmp  22030  kgenhaus  22080  pthaus  22174  txhaus  22183  xkohaus  22189  haushmph  22328  cmphaushmeo  22336  hausflim  22517  hauspwpwf1  22523  hauspwpwdom  22524  hausflf  22533  cnextfun  22600  cnextfvval  22601  cnextf  22602  cnextcn  22603  cnextfres1  22604  cnextfres  22605  qtophaus  30999  ismntop  31166  poimirlem30  34803  hausgraph  39690
  Copyright terms: Public domain W3C validator