Theorem haustop 23457

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095   ∩ cin 3910  ∅c0 4292  ∪ cuni 4874  Topctop 23019  Hauscha 23434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-ss 3928  df-uni 4875  df-haus 23441

This theorem is referenced by:  haust1  23478  resthaus  23494  sshaus  23501  lmmo  23506  hauscmplem  23532  hauscmp  23533  hauslly  23618  hausllycmp  23620  kgenhaus  23670  pthaus  23764  txhaus  23773  xkohaus  23779  haushmph  23918  cmphaushmeo  23926  hausflim  24107  hauspwpwf1  24113  hauspwpwdom  24114  hausflf  24123  cnextfun  24190  cnextfvval  24191  cnextf  24192  cnextcn  24193  cnextfres1  24194  cnextfres  24195  qtophaus  34171  ismntop  34361  poimirlem30  38224  hausgraph  43859