Metamath Proof Explorer

Theorem ist1-3

Description: A space is T_1 iff every point is the only point in the intersection of all open sets containing that point. (Contributed by Jeff Hankins, 31-Jan-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ist1-3 ⊢J∈TopOn⁡X→J∈Fre↔∀x∈X⋂o∈J|x∈o=x

Proof

Step Hyp Ref Expression
1 ist1-2 ⊢J∈TopOn⁡X→J∈Fre↔∀x∈X∀y∈X∀o∈Jx∈o→y∈o→x=y
2 toponmax ⊢J∈TopOn⁡X→X∈J
3 eleq2 ⊢o=X→x∈o↔x∈X
4 3 intminss ⊢X∈J∧x∈X→⋂o∈J|x∈o⊆X
5 2 4 sylan ⊢J∈TopOn⁡X∧x∈X→⋂o∈J|x∈o⊆X
6 5 sselda ⊢J∈TopOn⁡X∧x∈X∧y∈⋂o∈J|x∈o→y∈X
7 biimt ⊢y∈X→y∈x↔y∈X→y∈x
8 6 7 syl ⊢J∈TopOn⁡X∧x∈X∧y∈⋂o∈J|x∈o→y∈x↔y∈X→y∈x
9 8 ralbidva ⊢J∈TopOn⁡X∧x∈X→∀y∈⋂o∈J|x∈oy∈x↔∀y∈⋂o∈J|x∈oy∈X→y∈x
10 id ⊢x∈o→x∈o
11 10 rgenw ⊢∀o∈Jx∈o→x∈o
12 vex ⊢x∈V
13 12 elintrab ⊢x∈⋂o∈J|x∈o↔∀o∈Jx∈o→x∈o
14 11 13 mpbir ⊢x∈⋂o∈J|x∈o
15 snssi ⊢x∈⋂o∈J|x∈o→x⊆⋂o∈J|x∈o
16 14 15 ax-mp ⊢x⊆⋂o∈J|x∈o
17 eqss ⊢⋂o∈J|x∈o=x↔⋂o∈J|x∈o⊆x∧x⊆⋂o∈J|x∈o
18 16 17 mpbiran2 ⊢⋂o∈J|x∈o=x↔⋂o∈J|x∈o⊆x
19 dfss3 ⊢⋂o∈J|x∈o⊆x↔∀y∈⋂o∈J|x∈oy∈x
20 18 19 bitri ⊢⋂o∈J|x∈o=x↔∀y∈⋂o∈J|x∈oy∈x
21 vex ⊢y∈V
22 21 elintrab ⊢y∈⋂o∈J|x∈o↔∀o∈Jx∈o→y∈o
23 velsn ⊢y∈x↔y=x
24 equcom ⊢y=x↔x=y
25 23 24 bitri ⊢y∈x↔x=y
26 22 25 imbi12i ⊢y∈⋂o∈J|x∈o→y∈x↔∀o∈Jx∈o→y∈o→x=y
27 26 ralbii ⊢∀y∈Xy∈⋂o∈J|x∈o→y∈x↔∀y∈X∀o∈Jx∈o→y∈o→x=y
28 ralcom3 ⊢∀y∈Xy∈⋂o∈J|x∈o→y∈x↔∀y∈⋂o∈J|x∈oy∈X→y∈x
29 27 28 bitr3i ⊢∀y∈X∀o∈Jx∈o→y∈o→x=y↔∀y∈⋂o∈J|x∈oy∈X→y∈x
30 9 20 29 3bitr4g ⊢J∈TopOn⁡X∧x∈X→⋂o∈J|x∈o=x↔∀y∈X∀o∈Jx∈o→y∈o→x=y
31 30 ralbidva ⊢J∈TopOn⁡X→∀x∈X⋂o∈J|x∈o=x↔∀x∈X∀y∈X∀o∈Jx∈o→y∈o→x=y
32 1 31 bitr4d ⊢J∈TopOn⁡X→J∈Fre↔∀x∈X⋂o∈J|x∈o=x