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