Theorem haustop 23304

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2931  ∀wral 3050  ∃wrex 3059   ∩ cin 3932  ∅c0 4315  ∪ cuni 4889  Topctop 22866  Hauscha 23281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-ss 3950  df-uni 4890  df-haus 23288

This theorem is referenced by:  haust1  23325  resthaus  23341  sshaus  23348  lmmo  23353  hauscmplem  23379  hauscmp  23380  hauslly  23465  hausllycmp  23467  kgenhaus  23517  pthaus  23611  txhaus  23620  xkohaus  23626  haushmph  23765  cmphaushmeo  23773  hausflim  23954  hauspwpwf1  23960  hauspwpwdom  23961  hausflf  23970  cnextfun  24037  cnextfvval  24038  cnextf  24039  cnextcn  24040  cnextfres1  24041  cnextfres  24042  qtophaus  33776  ismntop  33968  poimirlem30  37598  hausgraph  43162