![]() |
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 2825 | . . 3 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | ishaus 21497 | . 2 ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ ∪ 𝐽∀𝑦 ∈ ∪ 𝐽(𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅)))) |
3 | 2 | simplbi 493 | 1 ⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1113 = wceq 1658 ∈ wcel 2166 ≠ wne 2999 ∀wral 3117 ∃wrex 3118 ∩ cin 3797 ∅c0 4144 ∪ cuni 4658 Topctop 21068 Hauscha 21483 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-uni 4659 df-haus 21490 |
This theorem is referenced by: haust1 21527 resthaus 21543 sshaus 21550 lmmo 21555 hauscmplem 21580 hauscmp 21581 hauslly 21666 hausllycmp 21668 kgenhaus 21718 pthaus 21812 txhaus 21821 xkohaus 21827 haushmph 21966 cmphaushmeo 21974 hausflim 22155 hauspwpwf1 22161 hauspwpwdom 22162 hausflf 22171 cnextfun 22238 cnextfvval 22239 cnextf 22240 cnextcn 22241 cnextfres1 22242 cnextfres 22243 qtophaus 30448 ismntop 30615 poimirlem30 33983 hausgraph 38633 |
Copyright terms: Public domain | W3C validator |