Theorem haustop 23557

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  ∃wrex 3088   ∩ cin 3901  ∅c0 4282  ∪ cuni 4870  Topctop 23119  Hauscha 23534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-uni 4871  df-haus 23541

This theorem is used by:  haust1  23578  resthaus  23594  sshaus  23601  lmmo  23606  hauscmplem  23632  hauscmp  23633  hauslly  23719  hausllycmp  23721  kgenhaus  23771  pthaus  23865  txhaus  23874  xkohaus  23880  haushmph  24019  cmphaushmeo  24027  hausflim  24208  hauspwpwf1  24214  hauspwpwdom  24215  hausflf  24224  cnextfun  24291  cnextfvval  24292  cnextf  24293  cnextcn  24294  cnextfres1  24295  cnextfres  24296  qtophaus  34333  ismntop  34523  poimirlem30  38386  hausgraph  44033