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

Metamath Proof Explorer

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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜 ) → 𝐴 = 𝐵 ) )