![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > haustop | Structured version Visualization version GIF version |
Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.) |
Ref | Expression |
---|---|
haustop | ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2771 | . . 3 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | ishaus 21347 | . 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
3 | 2 | simplbi 485 | 1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∃wrex 3062 ∩ cin 3722 ∅c0 4063 ∪ cuni 4574 Topctop 20918 Hauscha 21333 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-uni 4575 df-haus 21340 |
This theorem is referenced by: haust1 21377 resthaus 21393 sshaus 21400 lmmo 21405 hauscmplem 21430 hauscmp 21431 hauslly 21516 hausllycmp 21518 kgenhaus 21568 pthaus 21662 txhaus 21671 xkohaus 21677 haushmph 21816 cmphaushmeo 21824 hausflim 22005 hauspwpwf1 22011 hauspwpwdom 22012 hausflf 22021 cnextfun 22088 cnextfvval 22089 cnextf 22090 cnextcn 22091 cnextfres1 22092 cnextfres 22093 qtophaus 30243 ismntop 30410 poimirlem30 33772 hausgraph 38316 |
Copyright terms: Public domain | W3C validator |