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 ⊢ X = ⋃ J
Assertion t1sep2 ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X → ∀ o ∈ J A ∈ o → B ∈ o → A = B

Proof

Step Hyp Ref Expression
1 t1sep.1 ⊢ X = ⋃ J
2 t1top ⊢ J ∈ Fre → J ∈ Top
3 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
4 2 3 sylib ⊢ J ∈ Fre → J ∈ TopOn ⁡ X
5 ist1-2 ⊢ J ∈ TopOn ⁡ X → J ∈ Fre ↔ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y
6 4 5 syl ⊢ J ∈ Fre → J ∈ Fre ↔ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y
7 6 ibi ⊢ J ∈ Fre → ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y
8 eleq1 ⊢ x = A → x ∈ o ↔ A ∈ o
9 8 imbi1d ⊢ x = A → x ∈ o → y ∈ o ↔ A ∈ o → y ∈ o
10 9 ralbidv ⊢ x = A → ∀ o ∈ J x ∈ o → y ∈ o ↔ ∀ o ∈ J A ∈ o → y ∈ o
11 eqeq1 ⊢ x = A → x = y ↔ A = y
12 10 11 imbi12d ⊢ x = A → ∀ o ∈ J x ∈ o → y ∈ o → x = y ↔ ∀ o ∈ J A ∈ o → y ∈ o → A = y
13 eleq1 ⊢ y = B → y ∈ o ↔ B ∈ o
14 13 imbi2d ⊢ y = B → A ∈ o → y ∈ o ↔ A ∈ o → B ∈ o
15 14 ralbidv ⊢ y = B → ∀ o ∈ J A ∈ o → y ∈ o ↔ ∀ o ∈ J A ∈ o → B ∈ o
16 eqeq2 ⊢ y = B → A = y ↔ A = B
17 15 16 imbi12d ⊢ y = B → ∀ o ∈ J A ∈ o → y ∈ o → A = y ↔ ∀ o ∈ J A ∈ o → B ∈ o → A = B
18 12 17 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y → ∀ o ∈ J A ∈ o → B ∈ o → A = B
19 7 18 mpan9 ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X → ∀ o ∈ J A ∈ o → B ∈ o → A = B
20 19 3impb ⊢ J ∈ Fre ∧ A ∈ X ∧ B ∈ X → ∀ o ∈ J A ∈ o → B ∈ o → A = B