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

Theorem fclsfnflim 24017
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 23841 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
21adantr 479 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
3 fclstop 24001 . . . . . . . . . 10 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
43adantl 480 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ Top)
5 eqid 2726 . . . . . . . . . 10 𝐽 = 𝐽
65neisspw 23097 . . . . . . . . 9 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
74, 6syl 17 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
8 filunibas 23871 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = 𝑋)
95fclsfil 24000 . . . . . . . . . . 11 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 ∈ (Fil‘ 𝐽))
10 filunibas 23871 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘ 𝐽) → 𝐹 = 𝐽)
119, 10syl 17 . . . . . . . . . 10 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 = 𝐽)
128, 11sylan9req 2787 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝑋 = 𝐽)
1312pweqd 4615 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝒫 𝑋 = 𝒫 𝐽)
147, 13sseqtrrd 4021 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
152, 14unssd 4185 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋)
16 ssun1 4171 . . . . . . . 8 𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴}))
17 filn0 23852 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
18 ssn0 4399 . . . . . . . 8 ((𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
1916, 17, 18sylancr 585 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
2019adantr 479 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
21 incom 4200 . . . . . . . . . . . 12 (𝑦𝑥) = (𝑥𝑦)
22 fclsneii 24007 . . . . . . . . . . . 12 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥𝐹) → (𝑦𝑥) ≠ ∅)
2321, 22eqnetrrid 3006 . . . . . . . . . . 11 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥𝐹) → (𝑥𝑦) ≠ ∅)
24233com23 1123 . . . . . . . . . 10 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥𝑦) ≠ ∅)
25243expb 1117 . . . . . . . . 9 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥𝑦) ≠ ∅)
2625adantll 712 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) ∧ (𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥𝑦) ≠ ∅)
2726ralrimivva 3191 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅)
28 filfbas 23838 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
2928adantr 479 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
30 istopon 22900 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
314, 12, 30sylanbrc 581 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ (TopOn‘𝑋))
325fclselbas 24006 . . . . . . . . . . . . 13 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 𝐽)
3332adantl 480 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 𝐽)
3433, 12eleqtrrd 2829 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴𝑋)
3534snssd 4809 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ⊆ 𝑋)
36 snnzg 4774 . . . . . . . . . . 11 (𝐴 ∈ (𝐽 fClus 𝐹) → {𝐴} ≠ ∅)
3736adantl 480 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ≠ ∅)
38 neifil 23870 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
3931, 35, 37, 38syl3anc 1368 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
40 filfbas 23838 . . . . . . . . 9 (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
4139, 40syl 17 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
42 fbunfip 23859 . . . . . . . 8 ((𝐹 ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅))
4329, 41, 42syl2anc 582 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅))
4427, 43mpbird 256 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
45 filtop 23845 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
46 fsubbas 23857 . . . . . . . 8 (𝑋𝐹 → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4745, 46syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4847adantr 479 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4915, 20, 44, 48mpbir3and 1339 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋))
50 fgcl 23868 . . . . 5 ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
5149, 50syl 17 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
52 fvex 6904 . . . . . . . . 9 ((nei‘𝐽)‘{𝐴}) ∈ V
53 unexg 7747 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ V) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
5452, 53mpan2 689 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
55 ssfii 9453 . . . . . . . 8 ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5654, 55syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5756adantr 479 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5857unssad 4186 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
59 ssfg 23862 . . . . . 6 ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6049, 59syl 17 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6158, 60sstrd 3990 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6257unssbd 4187 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
6362, 60sstrd 3990 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
64 elflim 23961 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
6531, 51, 64syl2anc 582 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
6634, 63, 65mpbir2and 711 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
67 sseq2 4006 . . . . . 6 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
68 oveq2 7422 . . . . . . 7 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐽 fLim 𝑔) = (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
6968eleq2d 2812 . . . . . 6 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐴 ∈ (𝐽 fLim 𝑔) ↔ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
7067, 69anbi12d 630 . . . . 5 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → ((𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))))
7170rspcev 3608 . . . 4 (((𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))
7251, 61, 66, 71syl12anc 835 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))
7372ex 411 . 2 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔))))
74 simprl 769 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝑔 ∈ (Fil‘𝑋))
75 simprrr 780 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
76 flimtopon 23960 . . . . . . 7 (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
7775, 76syl 17 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
7874, 77mpbird 256 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐽 ∈ (TopOn‘𝑋))
79 simpl 481 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹 ∈ (Fil‘𝑋))
80 simprrl 779 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹𝑔)
81 fclsss2 24013 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
8278, 79, 80, 81syl3anc 1368 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
83 flimfcls 24016 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
8483, 75sselid 3977 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝑔))
8582, 84sseldd 3980 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝐹))
8685rexlimdvaa 3146 . 2 (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)) → 𝐴 ∈ (𝐽 fClus 𝐹)))
8773, 86impbid 211 1 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wral 3051  wrex 3060  Vcvv 3463  cun 3945  cin 3946  wss 3947  c0 4323  𝒫 cpw 4598  {csn 4624   cuni 4906  cfv 6544  (class class class)co 7414  ficfi 9444  fBascfbas 21325  filGencfg 21326  Topctop 22881  TopOnctopon 22898  neicnei 23087  Filcfil 23835   fLim cflim 23924   fClus cfcls 23926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7736
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3366  df-rab 3421  df-v 3465  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-int 4948  df-iun 4996  df-iin 4997  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-ord 6369  df-on 6370  df-lim 6371  df-suc 6372  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7867  df-1o 8486  df-2o 8487  df-en 8965  df-fin 8968  df-fi 9445  df-fbas 21334  df-fg 21335  df-top 22882  df-topon 22899  df-cld 23009  df-ntr 23010  df-cls 23011  df-nei 23088  df-fil 23836  df-flim 23929  df-fcls 23931
This theorem is referenced by:  uffclsflim  24021  cnpfcfi  24030
  Copyright terms: Public domain W3C validator