Metamath Proof Explorer

Theorem t1t0

Description: A T_1 space is a T_0 space. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion t1t0 ⊢ J ∈ Fre → J ∈ Kol2

Proof

Step Hyp Ref Expression
1 t1top ⊢ J ∈ Fre → J ∈ Top
2 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
3 1 2 sylib ⊢ J ∈ Fre → J ∈ TopOn ⁡ ⋃ J
4 biimp ⊢ x ∈ o ↔ y ∈ o → x ∈ o → y ∈ o
5 4 ralimi ⊢ ∀ o ∈ J x ∈ o ↔ y ∈ o → ∀ o ∈ J x ∈ o → y ∈ o
6 5 imim1i ⊢ ∀ o ∈ J x ∈ o → y ∈ o → x = y → ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
7 6 ralimi ⊢ ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o → y ∈ o → x = y → ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
8 7 ralimi ⊢ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o → y ∈ o → x = y → ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
9 8 a1i ⊢ J ∈ TopOn ⁡ ⋃ J → ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o → y ∈ o → x = y → ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
10 ist1-2 ⊢ J ∈ TopOn ⁡ ⋃ J → J ∈ Fre ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o → y ∈ o → x = y
11 ist0-2 ⊢ J ∈ TopOn ⁡ ⋃ J → J ∈ Kol2 ↔ ∀ x ∈ ⋃ J ∀ y ∈ ⋃ J ∀ o ∈ J x ∈ o ↔ y ∈ o → x = y
12 9 10 11 3imtr4d ⊢ J ∈ TopOn ⁡ ⋃ J → J ∈ Fre → J ∈ Kol2
13 3 12 mpcom ⊢ J ∈ Fre → J ∈ Kol2