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 ∈ J x ∈ 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 ∈ o y ∈ x ↔ ∀ y ∈ ⋂ o ∈ J | x ∈ o y ∈ X → y ∈ x
10 id ⊢ x ∈ o → x ∈ o
11 10 rgenw ⊢ ∀ o ∈ J x ∈ o → x ∈ o
12 vex ⊢ x ∈ V
13 12 elintrab ⊢ x ∈ ⋂ o ∈ J | x ∈ o ↔ ∀ o ∈ J x ∈ 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 ∈ o y ∈ x
20 18 19 bitri ⊢ ⋂ o ∈ J | x ∈ o = x ↔ ∀ y ∈ ⋂ o ∈ J | x ∈ o y ∈ x
21 vex ⊢ y ∈ V
22 21 elintrab ⊢ y ∈ ⋂ o ∈ J | x ∈ o ↔ ∀ o ∈ J x ∈ 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 ∈ J x ∈ o → y ∈ o → x = y
27 26 ralbii ⊢ ∀ y ∈ X y ∈ ⋂ o ∈ J | x ∈ o → y ∈ x ↔ ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y
28 ralcom3 ⊢ ∀ y ∈ X y ∈ ⋂ o ∈ J | x ∈ o → y ∈ x ↔ ∀ y ∈ ⋂ o ∈ J | x ∈ o y ∈ X → y ∈ x
29 27 28 bitr3i ⊢ ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y ↔ ∀ y ∈ ⋂ o ∈ J | x ∈ o y ∈ X → y ∈ x
30 9 20 29 3bitr4g ⊢ J ∈ TopOn ⁡ X ∧ x ∈ X → ⋂ o ∈ J | x ∈ o = x ↔ ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y
31 30 ralbidva ⊢ J ∈ TopOn ⁡ X → ∀ x ∈ X ⋂ o ∈ J | x ∈ o = x ↔ ∀ x ∈ X ∀ y ∈ X ∀ o ∈ J x ∈ o → y ∈ o → x = y
32 1 31 bitr4d ⊢ J ∈ TopOn ⁡ X → J ∈ Fre ↔ ∀ x ∈ X ⋂ o ∈ J | x ∈ o = x