Description: A regular space is R_1, which means that any two topologically distinct points can be separated by neighborhoods. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | regr1 | ⊢ ( 𝐽 ∈ Reg → ( KQ ‘ 𝐽 ) ∈ Haus ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | regtop | ⊢ ( 𝐽 ∈ Reg → 𝐽 ∈ Top ) | |
2 | toptopon2 | ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) | |
3 | 1 2 | sylib | ⊢ ( 𝐽 ∈ Reg → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
4 | eqid | ⊢ ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) | |
5 | 4 | regr1lem2 | ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐽 ∈ Reg ) → ( KQ ‘ 𝐽 ) ∈ Haus ) |
6 | 3 5 | mpancom | ⊢ ( 𝐽 ∈ Reg → ( KQ ‘ 𝐽 ) ∈ Haus ) |