Theorem haustop 23318

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

Syntax hints:   → wi 4   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121   ≠ wne 2936  ∀wral 3055  ∃wrex 3065   ∩ cin 3884  ∅c0 4264  ∪ cuni 4841  Topctop 22880  Hauscha 23295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-ss 3902  df-uni 4842  df-haus 23302

This theorem is referenced by:  haust1  23339  resthaus  23355  sshaus  23362  lmmo  23367  hauscmplem  23393  hauscmp  23394  hauslly  23479  hausllycmp  23481  kgenhaus  23531  pthaus  23625  txhaus  23634  xkohaus  23640  haushmph  23779  cmphaushmeo  23787  hausflim  23968  hauspwpwf1  23974  hauspwpwdom  23975  hausflf  23984  cnextfun  24051  cnextfvval  24052  cnextf  24053  cnextcn  24054  cnextfres1  24055  cnextfres  24056  qtophaus  34032  ismntop  34222  poimirlem30  38032  hausgraph  43665