Theorem t1t0

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

	Ref	Expression
Assertion	t1t0	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 )

Proof

Step	Hyp	Ref	Expression
1		t1top	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
2		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
3	1 2	sylib	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
4		biimp	⊢ ( ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) )
5	4	ralimi	⊢ ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) )
6	5	imim1i	⊢ ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) )
7	6	ralimi	⊢ ( ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) → ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) )
8	7	ralimi	⊢ ( ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) → ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) )
9	8	a1i	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) → ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
10		ist1-2	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
11		ist0-2	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
12	9 10 11	3imtr4d	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 ) )
13	3 12	mpcom	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Kol2 )