Metamath Proof Explorer

Theorem ist0cld

Description: The predicate "is a T_0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020)

Ref Expression
Hypotheses ist0cls.1 ⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
ist0cls.2 ⊢ ( 𝜑 → 𝐷 = ( Clsd ‘ 𝐽 ) )
Assertion ist0cld ( 𝜑 → ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 ist0cls.1 ⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
2 ist0cls.2 ⊢ ( 𝜑 → 𝐷 = ( Clsd ‘ 𝐽 ) )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 ist0 ⊢ ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
5 4 simplbi ⊢ ( 𝐽 ∈ Kol2 → 𝐽 ∈ Top )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Kol2 ) → 𝐽 ∈ Top )
7 4 baib ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ) )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → 𝐵 = ∪ 𝐽 )
10 9 eqcomd ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ∪ 𝐽 = 𝐵 )
11 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ∪ 𝐽 = 𝐵 )
12 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) → 𝐽 ∈ Top )
13 uniexg ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
14 difexg ⊢ ( ∪ 𝐽 ∈ V → ( ∪ 𝐽 ∖ 𝑜 ) ∈ V )
15 12 13 14 3syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑜 ) ∈ V )
16 3 iscld ⊢ ( 𝐽 ∈ Top → ( 𝑑 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑑 ⊆ ∪ 𝐽 ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( 𝑑 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑑 ⊆ ∪ 𝐽 ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) ) )
18 2 eleq2d ⊢ ( 𝜑 → ( 𝑑 ∈ 𝐷 ↔ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( 𝑑 ∈ 𝐷 ↔ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ) )
20 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) )
21 difssd ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ∪ 𝐽 ∖ 𝑜 ) ⊆ ∪ 𝐽 )
22 20 21 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → 𝑑 ⊆ ∪ 𝐽 )
23 22 r19.29an ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ ∃ 𝑜 ∈ 𝐽 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → 𝑑 ⊆ ∪ 𝐽 )
24 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) )
25 24 difeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ∪ 𝐽 ∖ 𝑑 ) = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑜 ) ) )
26 3 eltopss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ) → 𝑜 ⊆ ∪ 𝐽 )
27 26 ad5ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → 𝑜 ⊆ ∪ 𝐽 )
28 dfss4 ⊢ ( 𝑜 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑜 ) ) = 𝑜 )
29 27 28 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑜 ) ) = 𝑜 )
30 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → 𝑜 ∈ 𝐽 )
31 29 30 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑜 ) ) ∈ 𝐽 )
32 25 31 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 )
33 32 r19.29an ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ∃ 𝑜 ∈ 𝐽 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 )
34 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 )
35 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) ∧ 𝑜 = ( ∪ 𝐽 ∖ 𝑑 ) ) → 𝑜 = ( ∪ 𝐽 ∖ 𝑑 ) )
36 35 difeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) ∧ 𝑜 = ( ∪ 𝐽 ∖ 𝑑 ) ) → ( ∪ 𝐽 ∖ 𝑜 ) = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑑 ) ) )
37 36 eqeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) ∧ 𝑜 = ( ∪ 𝐽 ∖ 𝑑 ) ) → ( 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ↔ 𝑑 = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑑 ) ) ) )
38 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) → 𝑑 ⊆ ∪ 𝐽 )
39 dfss4 ⊢ ( 𝑑 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑑 ) ) = 𝑑 )
40 38 39 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑑 ) ) = 𝑑 )
41 40 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) → 𝑑 = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑑 ) ) )
42 34 37 41 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) → ∃ 𝑜 ∈ 𝐽 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) )
43 33 42 impbida ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑑 ⊆ ∪ 𝐽 ) → ( ∃ 𝑜 ∈ 𝐽 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ↔ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) )
44 23 43 biadanid ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( ∃ 𝑜 ∈ 𝐽 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ↔ ( 𝑑 ⊆ ∪ 𝐽 ∧ ( ∪ 𝐽 ∖ 𝑑 ) ∈ 𝐽 ) ) )
45 17 19 44 3bitr4d ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( 𝑑 ∈ 𝐷 ↔ ∃ 𝑜 ∈ 𝐽 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) )
46 45 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) → ( 𝑑 ∈ 𝐷 ↔ ∃ 𝑜 ∈ 𝐽 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) )
47 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) )
48 47 eleq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( 𝑥 ∈ 𝑑 ↔ 𝑥 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ) )
49 eldif ⊢ ( 𝑥 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ¬ 𝑥 ∈ 𝑜 ) )
50 49 baib ⊢ ( 𝑥 ∈ ∪ 𝐽 → ( 𝑥 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ↔ ¬ 𝑥 ∈ 𝑜 ) )
51 50 ad3antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( 𝑥 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ↔ ¬ 𝑥 ∈ 𝑜 ) )
52 48 51 bitrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( 𝑥 ∈ 𝑑 ↔ ¬ 𝑥 ∈ 𝑜 ) )
53 47 eleq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( 𝑦 ∈ 𝑑 ↔ 𝑦 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ) )
54 eldif ⊢ ( 𝑦 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ↔ ( 𝑦 ∈ ∪ 𝐽 ∧ ¬ 𝑦 ∈ 𝑜 ) )
55 54 baib ⊢ ( 𝑦 ∈ ∪ 𝐽 → ( 𝑦 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ↔ ¬ 𝑦 ∈ 𝑜 ) )
56 55 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( 𝑦 ∈ ( ∪ 𝐽 ∖ 𝑜 ) ↔ ¬ 𝑦 ∈ 𝑜 ) )
57 53 56 bitrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( 𝑦 ∈ 𝑑 ↔ ¬ 𝑦 ∈ 𝑜 ) )
58 52 57 bibi12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ↔ ( ¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜 ) ) )
59 notbi ⊢ ( ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ( ¬ 𝑥 ∈ 𝑜 ↔ ¬ 𝑦 ∈ 𝑜 ) )
60 58 59 bitr4di ⊢ ( ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) ∧ 𝑑 = ( ∪ 𝐽 ∖ 𝑜 ) ) → ( ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ↔ ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) )
61 15 46 60 ralxfr2d ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) → ( ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ) )
62 61 bicomd ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) ↔ ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) ) )
63 62 imbi1d ⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) ∧ 𝑦 ∈ ∪ 𝐽 ) → ( ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ( ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) )
64 11 63 raleqbidva ⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ Top ) ∧ 𝑥 ∈ ∪ 𝐽 ) → ( ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) )
65 10 64 raleqbidva ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑜 ∈ 𝐽 ( 𝑥 ∈ 𝑜 ↔ 𝑦 ∈ 𝑜 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) )
66 8 65 bitrd ⊢ ( ( 𝜑 ∧ 𝐽 ∈ Top ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) )
67 6 66 biadanid ⊢ ( 𝜑 → ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑑 ∈ 𝐷 ( 𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑 ) → 𝑥 = 𝑦 ) ) ) )