Theorem t0sep

Description: Any two topologically indistinguishable points in a T_0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	ist0.1	⊢ 𝑋 = ∪ 𝐽
Assertion	t0sep	⊢ ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) → 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	⊢ 𝑋 = ∪ 𝐽
2	1	ist0	⊢ ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝐽 ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) → 𝑦 = 𝑧 ) ) )
3	2	simprbi	⊢ ( 𝐽 ∈ Kol2 → ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝐽 ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) → 𝑦 = 𝑧 ) )
4		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
5	4	bibi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) ↔ ( 𝐴 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) ) )
6	5	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝐽 ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) ) )
7		eqeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝑧 ↔ 𝐴 = 𝑧 ) )
8	6 7	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝐽 ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) → 𝑦 = 𝑧 ) ↔ ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) → 𝐴 = 𝑧 ) ) )
9		eleq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) )
10	9	bibi2d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) ↔ ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) ) )
11	10	ralbidv	⊢ ( 𝑧 = 𝐵 → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) ) )
12		eqeq2	⊢ ( 𝑧 = 𝐵 → ( 𝐴 = 𝑧 ↔ 𝐴 = 𝐵 ) )
13	11 12	imbi12d	⊢ ( 𝑧 = 𝐵 → ( ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) → 𝐴 = 𝑧 ) ↔ ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) → 𝐴 = 𝐵 ) ) )
14	8 13	rspc2va	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝐽 ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) → 𝑦 = 𝑧 ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) → 𝐴 = 𝐵 ) )
15	14	ancoms	⊢ ( ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝐽 ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) → 𝑦 = 𝑧 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) → 𝐴 = 𝐵 ) )
16	3 15	sylan	⊢ ( ( 𝐽 ∈ Kol2 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ↔ 𝐵 ∈ 𝑥 ) → 𝐴 = 𝐵 ) )