Theorem t1sep2

Description: Any two points in a T_1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010)

	Ref	Expression
Hypothesis	t1sep.1	⊢ 𝑋 = ∪ 𝐽
Assertion	t1sep2	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	⊢ 𝑋 = ∪ 𝐽
2		t1top	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
3	1	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4	2 3	sylib	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5		ist1-2	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
6	4 5	syl	⊢ ( 𝐽 ∈ Fre → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
7	6	ibi	⊢ ( 𝐽 ∈ Fre → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) )
8		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜 ) )
9	8	imbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ) )
10	9	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ) )
11		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝐴 = 𝑦 ) )
12	10 11	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝐴 = 𝑦 ) ) )
13		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜 ) )
14	13	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) )
15	14	ralbidv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) ) )
16		eqeq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 = 𝑦 ↔ 𝐴 = 𝐵 ) )
17	15 16	imbi12d	⊢ ( 𝑦 = 𝐵 → ( ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝐴 = 𝑦 ) ↔ ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) ) )
18	12 17	rspc2v	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) ) )
19	7 18	mpan9	⊢ ( ( 𝐽 ∈ Fre ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) )
20	19	3impb	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) )