Theorem haustop 21936

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 2798	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	ishaus 21927	. 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
3	2	simplbi 501	1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top)

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ∩ cin 3880  ∅c0 4243  ∪ cuni 4800  Topctop 21498  Hauscha 21913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-haus 21920

This theorem is referenced by:  haust1  21957  resthaus  21973  sshaus  21980  lmmo  21985  hauscmplem  22011  hauscmp  22012  hauslly  22097  hausllycmp  22099  kgenhaus  22149  pthaus  22243  txhaus  22252  xkohaus  22258  haushmph  22397  cmphaushmeo  22405  hausflim  22586  hauspwpwf1  22592  hauspwpwdom  22593  hausflf  22602  cnextfun  22669  cnextfvval  22670  cnextf  22671  cnextcn  22672  cnextfres1  22673  cnextfres  22674  qtophaus  31189  ismntop  31377  poimirlem30  35087  hausgraph  40156