MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fclsfnflim Structured version   Visualization version   GIF version

Theorem fclsfnflim 22208
Description: A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
Assertion
Ref Expression
fclsfnflim (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔))))
Distinct variable groups:   𝐴,𝑔   𝑔,𝐹   𝑔,𝐽   𝑔,𝑋

Proof of Theorem fclsfnflim
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 filsspw 22032 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
21adantr 474 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
3 fclstop 22192 . . . . . . . . . 10 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
43adantl 475 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ Top)
5 eqid 2825 . . . . . . . . . 10 𝐽 = 𝐽
65neisspw 21289 . . . . . . . . 9 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
74, 6syl 17 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
8 filunibas 22062 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = 𝑋)
95fclsfil 22191 . . . . . . . . . . 11 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 ∈ (Fil‘ 𝐽))
10 filunibas 22062 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘ 𝐽) → 𝐹 = 𝐽)
119, 10syl 17 . . . . . . . . . 10 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 = 𝐽)
128, 11sylan9req 2882 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝑋 = 𝐽)
1312pweqd 4385 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝒫 𝑋 = 𝒫 𝐽)
147, 13sseqtr4d 3867 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
152, 14unssd 4018 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋)
16 ssun1 4005 . . . . . . . 8 𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴}))
17 filn0 22043 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
18 ssn0 4203 . . . . . . . 8 ((𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
1916, 17, 18sylancr 581 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
2019adantr 474 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
21 incom 4034 . . . . . . . . . . . 12 (𝑦𝑥) = (𝑥𝑦)
22 fclsneii 22198 . . . . . . . . . . . 12 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥𝐹) → (𝑦𝑥) ≠ ∅)
2321, 22syl5eqner 3074 . . . . . . . . . . 11 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥𝐹) → (𝑥𝑦) ≠ ∅)
24233com23 1160 . . . . . . . . . 10 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥𝑦) ≠ ∅)
25243expb 1153 . . . . . . . . 9 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥𝑦) ≠ ∅)
2625adantll 705 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) ∧ (𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥𝑦) ≠ ∅)
2726ralrimivva 3180 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅)
28 filfbas 22029 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
2928adantr 474 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
30 istopon 21094 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
314, 12, 30sylanbrc 578 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ (TopOn‘𝑋))
325fclselbas 22197 . . . . . . . . . . . . 13 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 𝐽)
3332adantl 475 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 𝐽)
3433, 12eleqtrrd 2909 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴𝑋)
3534snssd 4560 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ⊆ 𝑋)
36 snnzg 4529 . . . . . . . . . . 11 (𝐴 ∈ (𝐽 fClus 𝐹) → {𝐴} ≠ ∅)
3736adantl 475 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ≠ ∅)
38 neifil 22061 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
3931, 35, 37, 38syl3anc 1494 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
40 filfbas 22029 . . . . . . . . 9 (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
4139, 40syl 17 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
42 fbunfip 22050 . . . . . . . 8 ((𝐹 ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅))
4329, 41, 42syl2anc 579 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅))
4427, 43mpbird 249 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
45 filtop 22036 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
46 fsubbas 22048 . . . . . . . 8 (𝑋𝐹 → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4745, 46syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4847adantr 474 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4915, 20, 44, 48mpbir3and 1446 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋))
50 fgcl 22059 . . . . 5 ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
5149, 50syl 17 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
52 fvex 6450 . . . . . . . . 9 ((nei‘𝐽)‘{𝐴}) ∈ V
53 unexg 7224 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ V) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
5452, 53mpan2 682 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
55 ssfii 8600 . . . . . . . 8 ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5654, 55syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5756adantr 474 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5857unssad 4019 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
59 ssfg 22053 . . . . . 6 ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6049, 59syl 17 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6158, 60sstrd 3837 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6257unssbd 4020 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
6362, 60sstrd 3837 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
64 elflim 22152 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
6531, 51, 64syl2anc 579 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
6634, 63, 65mpbir2and 704 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
67 sseq2 3852 . . . . . 6 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
68 oveq2 6918 . . . . . . 7 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐽 fLim 𝑔) = (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
6968eleq2d 2892 . . . . . 6 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐴 ∈ (𝐽 fLim 𝑔) ↔ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
7067, 69anbi12d 624 . . . . 5 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → ((𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))))
7170rspcev 3526 . . . 4 (((𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))
7251, 61, 66, 71syl12anc 870 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))
7372ex 403 . 2 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔))))
74 simprl 787 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝑔 ∈ (Fil‘𝑋))
75 simprrr 800 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
76 flimtopon 22151 . . . . . . 7 (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
7775, 76syl 17 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
7874, 77mpbird 249 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐽 ∈ (TopOn‘𝑋))
79 simpl 476 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹 ∈ (Fil‘𝑋))
80 simprrl 799 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹𝑔)
81 fclsss2 22204 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
8278, 79, 80, 81syl3anc 1494 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
83 flimfcls 22207 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
8483, 75sseldi 3825 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝑔))
8582, 84sseldd 3828 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝐹))
8685rexlimdvaa 3241 . 2 (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)) → 𝐴 ∈ (𝐽 fClus 𝐹)))
8773, 86impbid 204 1 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1111   = wceq 1656  wcel 2164  wne 2999  wral 3117  wrex 3118  Vcvv 3414  cun 3796  cin 3797  wss 3798  c0 4146  𝒫 cpw 4380  {csn 4399   cuni 4660  cfv 6127  (class class class)co 6910  ficfi 8591  fBascfbas 20101  filGencfg 20102  Topctop 21075  TopOnctopon 21092  neicnei 21279  Filcfil 22026   fLim cflim 22115   fClus cfcls 22117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-iin 4745  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-om 7332  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-oadd 7835  df-er 8014  df-en 8229  df-fin 8232  df-fi 8592  df-fbas 20110  df-fg 20111  df-top 21076  df-topon 21093  df-cld 21201  df-ntr 21202  df-cls 21203  df-nei 21280  df-fil 22027  df-flim 22120  df-fcls 22122
This theorem is referenced by:  uffclsflim  22212  cnpfcfi  22221
  Copyright terms: Public domain W3C validator