Theorem haustop 23596

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 2760	. . 3 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	ishaus 23587	. 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 2955  ∀wral 3076  ∃wrex 3086   ∩ cin 3898  ∅c0 4279  ∪ cuni 4867  Topctop 23158  Hauscha 23573

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3916  df-uni 4868  df-haus 23580

This theorem is used by:  haust1  23617  resthaus  23633  sshaus  23640  lmmo  23645  hauscmplem  23671  hauscmp  23672  hauslly  23758  hausllycmp  23760  kgenhaus  23810  pthaus  23904  txhaus  23913  xkohaus  23919  haushmph  24058  cmphaushmeo  24066  hausflim  24247  hauspwpwf1  24253  hauspwpwdom  24254  hausflf  24263  cnextfun  24330  cnextfvval  24331  cnextf  24332  cnextcn  24333  cnextfres1  24334  cnextfres  24335  qtophaus  34387  ismntop  34577  poimirlem30  38482  hausgraph  44144