Theorem haustop 23279

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.

Step	Hyp	Ref	Expression
1		eqid 2725	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	ishaus 23270	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
3	2	simplbi 496	1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2929  ∀wral 3050  ∃wrex 3059   ∩ cin 3943  ∅c0 4322  ∪ cuni 4909  Topctop 22839  Hauscha 23256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-ss 3961  df-uni 4910  df-haus 23263

This theorem is referenced by:  haust1  23300  resthaus  23316  sshaus  23323  lmmo  23328  hauscmplem  23354  hauscmp  23355  hauslly  23440  hausllycmp  23442  kgenhaus  23492  pthaus  23586  txhaus  23595  xkohaus  23601  haushmph  23740  cmphaushmeo  23748  hausflim  23929  hauspwpwf1  23935  hauspwpwdom  23936  hausflf  23945  cnextfun  24012  cnextfvval  24013  cnextf  24014  cnextcn  24015  cnextfres1  24016  cnextfres  24017  qtophaus  33568  ismntop  33758  poimirlem30  37254  hausgraph  42775