This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 ∈ 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 )