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 ↔ ∀ 𝑥𝑋 { 𝑜𝐽𝑥𝑜 } = { 𝑥 } ) )