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∈JA∈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∈Jx∈o→y∈o→x=y
6 4 5 syl ⊢J∈Fre→J∈Fre↔∀x∈X∀y∈X∀o∈Jx∈o→y∈o→x=y
7 6 ibi ⊢J∈Fre→∀x∈X∀y∈X∀o∈Jx∈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∈Jx∈o→y∈o↔∀o∈JA∈o→y∈o
11 eqeq1 ⊢x=A→x=y↔A=y
12 10 11 imbi12d ⊢x=A→∀o∈Jx∈o→y∈o→x=y↔∀o∈JA∈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∈JA∈o→y∈o↔∀o∈JA∈o→B∈o
16 eqeq2 ⊢y=B→A=y↔A=B
17 15 16 imbi12d ⊢y=B→∀o∈JA∈o→y∈o→A=y↔∀o∈JA∈o→B∈o→A=B
18 12 17 rspc2v ⊢A∈X∧B∈X→∀x∈X∀y∈X∀o∈Jx∈o→y∈o→x=y→∀o∈JA∈o→B∈o→A=B
19 7 18 mpan9 ⊢J∈Fre∧A∈X∧B∈X→∀o∈JA∈o→B∈o→A=B
20 19 3impb ⊢J∈Fre∧A∈X∧B∈X→∀o∈JA∈o→B∈o→A=B