Theorem haustop 23393

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

Syntax hints:   → wi 4   ∧ w3a 1099   = wceq 1562   ∈ wcel 2144   ≠ wne 2959  ∀wral 3078  ∃wrex 3088   ∩ cin 3905  ∅c0 4287  ∪ cuni 4867  Topctop 22955  Hauscha 23370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-ss 3923  df-uni 4868  df-haus 23377

This theorem is referenced by:  haust1  23414  resthaus  23430  sshaus  23437  lmmo  23442  hauscmplem  23468  hauscmp  23469  hauslly  23554  hausllycmp  23556  kgenhaus  23606  pthaus  23700  txhaus  23709  xkohaus  23715  haushmph  23854  cmphaushmeo  23862  hausflim  24043  hauspwpwf1  24049  hauspwpwdom  24050  hausflf  24059  cnextfun  24126  cnextfvval  24127  cnextf  24128  cnextcn  24129  cnextfres1  24130  cnextfres  24131  qtophaus  34135  ismntop  34325  poimirlem30  38154  hausgraph  43787