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

Theorem fclsfnflim 22563
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 22387 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
21adantr 481 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ 𝒫 𝑋)
3 fclstop 22547 . . . . . . . . . 10 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
43adantl 482 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ Top)
5 eqid 2818 . . . . . . . . . 10 𝐽 = 𝐽
65neisspw 21643 . . . . . . . . 9 (𝐽 ∈ Top → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
74, 6syl 17 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝐽)
8 filunibas 22417 . . . . . . . . . 10 (𝐹 ∈ (Fil‘𝑋) → 𝐹 = 𝑋)
95fclsfil 22546 . . . . . . . . . . 11 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 ∈ (Fil‘ 𝐽))
10 filunibas 22417 . . . . . . . . . . 11 (𝐹 ∈ (Fil‘ 𝐽) → 𝐹 = 𝐽)
119, 10syl 17 . . . . . . . . . 10 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 = 𝐽)
128, 11sylan9req 2874 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝑋 = 𝐽)
1312pweqd 4540 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝒫 𝑋 = 𝒫 𝐽)
147, 13sseqtrrd 4005 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋)
152, 14unssd 4159 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋)
16 ssun1 4145 . . . . . . . 8 𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴}))
17 filn0 22398 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
18 ssn0 4351 . . . . . . . 8 ((𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
1916, 17, 18sylancr 587 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
2019adantr 481 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅)
21 incom 4175 . . . . . . . . . . . 12 (𝑦𝑥) = (𝑥𝑦)
22 fclsneii 22553 . . . . . . . . . . . 12 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥𝐹) → (𝑦𝑥) ≠ ∅)
2321, 22eqnetrrid 3088 . . . . . . . . . . 11 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥𝐹) → (𝑥𝑦) ≠ ∅)
24233com23 1118 . . . . . . . . . 10 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥𝑦) ≠ ∅)
25243expb 1112 . . . . . . . . 9 ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥𝑦) ≠ ∅)
2625adantll 710 . . . . . . . 8 (((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) ∧ (𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥𝑦) ≠ ∅)
2726ralrimivva 3188 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅)
28 filfbas 22384 . . . . . . . . 9 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
2928adantr 481 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ∈ (fBas‘𝑋))
30 istopon 21448 . . . . . . . . . . 11 (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝐽))
314, 12, 30sylanbrc 583 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ (TopOn‘𝑋))
325fclselbas 22552 . . . . . . . . . . . . 13 (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 𝐽)
3332adantl 482 . . . . . . . . . . . 12 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 𝐽)
3433, 12eleqtrrd 2913 . . . . . . . . . . 11 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴𝑋)
3534snssd 4734 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ⊆ 𝑋)
36 snnzg 4702 . . . . . . . . . . 11 (𝐴 ∈ (𝐽 fClus 𝐹) → {𝐴} ≠ ∅)
3736adantl 482 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ≠ ∅)
38 neifil 22416 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
3931, 35, 37, 38syl3anc 1363 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋))
40 filfbas 22384 . . . . . . . . 9 (((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
4139, 40syl 17 . . . . . . . 8 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋))
42 fbunfip 22405 . . . . . . . 8 ((𝐹 ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅))
4329, 41, 42syl2anc 584 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥𝐹𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥𝑦) ≠ ∅))
4427, 43mpbird 258 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
45 filtop 22391 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
46 fsubbas 22403 . . . . . . . 8 (𝑋𝐹 → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4745, 46syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4847adantr 481 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
4915, 20, 44, 48mpbir3and 1334 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋))
50 fgcl 22414 . . . . 5 ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
5149, 50syl 17 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋))
52 fvex 6676 . . . . . . . . 9 ((nei‘𝐽)‘{𝐴}) ∈ V
53 unexg 7461 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ V) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
5452, 53mpan2 687 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V)
55 ssfii 8871 . . . . . . . 8 ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5654, 55syl 17 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5756adantr 481 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
5857unssad 4160 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
59 ssfg 22408 . . . . . 6 ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6049, 59syl 17 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6158, 60sstrd 3974 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
6257unssbd 4161 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))
6362, 60sstrd 3974 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))
64 elflim 22507 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
6531, 51, 64syl2anc 584 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))
6634, 63, 65mpbir2and 709 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
67 sseq2 3990 . . . . . 6 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐹𝑔𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
68 oveq2 7153 . . . . . . 7 (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐽 fLim 𝑔) = (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))
6968eleq2d 2895 . . . . . 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 3620 . . . 4 (((𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))
7251, 61, 66, 71syl12anc 832 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))
7372ex 413 . 2 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔))))
74 simprl 767 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝑔 ∈ (Fil‘𝑋))
75 simprrr 778 . . . . . . 7 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
76 flimtopon 22506 . . . . . . 7 (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
7775, 76syl 17 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋)))
7874, 77mpbird 258 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐽 ∈ (TopOn‘𝑋))
79 simpl 483 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹 ∈ (Fil‘𝑋))
80 simprrl 777 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹𝑔)
81 fclsss2 22559 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐹𝑔) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
8278, 79, 80, 81syl3anc 1363 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹))
83 flimfcls 22562 . . . . 5 (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔)
8483, 75sseldi 3962 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝑔))
8582, 84sseldd 3965 . . 3 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝐹))
8685rexlimdvaa 3282 . 2 (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔)) → 𝐴 ∈ (𝐽 fClus 𝐹)))
8773, 86impbid 213 1 (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹𝑔𝐴 ∈ (𝐽 fLim 𝑔))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  Vcvv 3492  cun 3931  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557   cuni 4830  cfv 6348  (class class class)co 7145  ficfi 8862  fBascfbas 20461  filGencfg 20462  Topctop 21429  TopOnctopon 21446  neicnei 21633  Filcfil 22381   fLim cflim 22470   fClus cfcls 22472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-en 8498  df-fin 8501  df-fi 8863  df-fbas 20470  df-fg 20471  df-top 21430  df-topon 21447  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-fil 22382  df-flim 22475  df-fcls 22477
This theorem is referenced by:  uffclsflim  22567  cnpfcfi  22576
  Copyright terms: Public domain W3C validator