Metamath Proof Explorer

Theorem ist1-2

Description: An alternate characterization of T_1 spaces. (Contributed by Jeff Hankins, 31-Jan-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ist1-2 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 2 ist1 ⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ ∪ 𝐽 { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ) )
4 3 baib ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Fre ↔ ∀ 𝑦 ∈ ∪ 𝐽 { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ) )
5 1 4 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑦 ∈ ∪ 𝐽 { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ) )
6 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
7 6 raleqdv ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑦 ∈ ∪ 𝐽 { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ) )
8 1 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝐽 ∈ Top )
9 eltop2 ⊢ ( 𝐽 ∈ Top → ( ( ∪ 𝐽 ∖ { 𝑦 } ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( ∪ 𝐽 ∖ { 𝑦 } ) ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) )
10 8 9 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( ∪ 𝐽 ∖ { 𝑦 } ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( ∪ 𝐽 ∖ { 𝑦 } ) ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) )
11 6 eleq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑦 ∈ 𝑋 ↔ 𝑦 ∈ ∪ 𝐽 ) )
12 11 biimpa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ ∪ 𝐽 )
13 12 snssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → { 𝑦 } ⊆ ∪ 𝐽 )
14 2 iscld2 ⊢ ( ( 𝐽 ∈ Top ∧ { 𝑦 } ⊆ ∪ 𝐽 ) → ( { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ { 𝑦 } ) ∈ 𝐽 ) )
15 8 13 14 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ { 𝑦 } ) ∈ 𝐽 ) )
16 6 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑋 = ∪ 𝐽 )
17 16 eleq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝐽 ) )
18 17 imbi1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 → ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ) ↔ ( 𝑥 ∈ ∪ 𝐽 → ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ) ) )
19 con1b ⊢ ( ( ¬ 𝑥 = 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ↔ ( ¬ ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) → 𝑥 = 𝑦 ) )
20 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
21 20 imbi1i ⊢ ( ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ↔ ( ¬ 𝑥 = 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) )
22 disjsn ⊢ ( ( 𝑜 ∩ { 𝑦 } ) = ∅ ↔ ¬ 𝑦 ∈ 𝑜 )
23 elssuni ⊢ ( 𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽 )
24 reldisj ⊢ ( 𝑜 ⊆ ∪ 𝐽 → ( ( 𝑜 ∩ { 𝑦 } ) = ∅ ↔ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) )
25 23 24 syl ⊢ ( 𝑜 ∈ 𝐽 → ( ( 𝑜 ∩ { 𝑦 } ) = ∅ ↔ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) )
26 22 25 bitr3id ⊢ ( 𝑜 ∈ 𝐽 → ( ¬ 𝑦 ∈ 𝑜 ↔ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) )
27 26 anbi2d ⊢ ( 𝑜 ∈ 𝐽 → ( ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ↔ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) )
28 27 rexbiia ⊢ ( ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ↔ ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) )
29 rexanali ⊢ ( ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜 ) ↔ ¬ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) )
30 28 29 bitr3i ⊢ ( ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ↔ ¬ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) )
31 30 con2bii ⊢ ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) ↔ ¬ ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) )
32 31 imbi1i ⊢ ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ( ¬ ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) → 𝑥 = 𝑦 ) )
33 19 21 32 3bitr4ri ⊢ ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) )
34 33 imbi2i ⊢ ( ( 𝑥 ∈ 𝑋 → ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑋 → ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ) )
35 eldifsn ⊢ ( 𝑥 ∈ ( ∪ 𝐽 ∖ { 𝑦 } ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) )
36 35 imbi1i ⊢ ( ( 𝑥 ∈ ( ∪ 𝐽 ∖ { 𝑦 } ) → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ↔ ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) )
37 impexp ⊢ ( ( ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ↔ ( 𝑥 ∈ ∪ 𝐽 → ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ) )
38 36 37 bitri ⊢ ( ( 𝑥 ∈ ( ∪ 𝐽 ∖ { 𝑦 } ) → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ↔ ( 𝑥 ∈ ∪ 𝐽 → ( 𝑥 ≠ 𝑦 → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ) )
39 18 34 38 3bitr4g ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 → ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝑥 ∈ ( ∪ 𝐽 ∖ { 𝑦 } ) → ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) ) )
40 39 ralbidv2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ ( ∪ 𝐽 ∖ { 𝑦 } ) ∃ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( ∪ 𝐽 ∖ { 𝑦 } ) ) ) )
41 10 15 40 3bitr4d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
42 41 ralbidva ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
43 ralcom ⊢ ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) )
44 42 43 bitrdi ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 { 𝑦 } ∈ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
45 5 7 44 3bitr2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Fre ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )