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

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 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 ist1-2 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
2 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
3 eleq2 ⊢ ( 𝑜 = 𝑋 → ( 𝑥 ∈ 𝑜 ↔ 𝑥 ∈ 𝑋 ) )
4 3 intminss ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝑥 ∈ 𝑋 ) → ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ 𝑋 )
5 2 4 sylan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ 𝑋 )
6 5 sselda ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ) → 𝑦 ∈ 𝑋 )
7 biimt ⊢ ( 𝑦 ∈ 𝑋 → ( 𝑦 ∈ { 𝑥 } ↔ ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) )
8 6 7 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ) → ( 𝑦 ∈ { 𝑥 } ↔ ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) )
9 8 ralbidva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } 𝑦 ∈ { 𝑥 } ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) ) )
10 id ⊢ ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜 )
11 10 rgenw ⊢ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜 )
12 vex ⊢ 𝑥 ∈ V
13 12 elintrab ⊢ ( 𝑥 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑥 ∈ 𝑜 ) )
14 11 13 mpbir ⊢ 𝑥 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 }
15 snssi ⊢ ( 𝑥 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → { 𝑥 } ⊆ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } )
16 14 15 ax-mp ⊢ { 𝑥 } ⊆ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 }
17 eqss ⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ { 𝑥 } ∧ { 𝑥 } ⊆ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ) )
18 16 17 mpbiran2 ⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ { 𝑥 } )
19 dfss3 ⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ⊆ { 𝑥 } ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } 𝑦 ∈ { 𝑥 } )
20 18 19 bitri ⊢ ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } 𝑦 ∈ { 𝑥 } )
21 vex ⊢ 𝑦 ∈ V
22 21 elintrab ⊢ ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) )
23 velsn ⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
24 equcom ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
25 23 24 bitri ⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑥 = 𝑦 )
26 22 25 imbi12i ⊢ ( ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → 𝑦 ∈ { 𝑥 } ) ↔ ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) )
27 26 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → 𝑦 ∈ { 𝑥 } ) ↔ ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) )
28 ralcom3 ⊢ ( ∀ 𝑦 ∈ 𝑋 ( 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } → 𝑦 ∈ { 𝑥 } ) ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) )
29 27 28 bitr3i ⊢ ( ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } ( 𝑦 ∈ 𝑋 → 𝑦 ∈ { 𝑥 } ) )
30 9 20 29 3bitr4g ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
31 30 ralbidva ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
32 1 31 bitr4d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∩ { 𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜 } = { 𝑥 } ) )