Step | Hyp | Ref
| Expression |
1 | | filsspw 21465 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) |
2 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ 𝒫 𝑋) |
3 | | fclstop 21625 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top) |
4 | 3 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ Top) |
5 | | eqid 2610 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
6 | 5 | neisspw 20721 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top →
((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽) |
7 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 ∪ 𝐽) |
8 | | filunibas 21495 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) |
9 | 5 | fclsfil 21624 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 ∈ (Fil‘∪ 𝐽)) |
10 | | filunibas 21495 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘∪ 𝐽)
→ ∪ 𝐹 = ∪ 𝐽) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → ∪ 𝐹 = ∪
𝐽) |
12 | 8, 11 | sylan9req 2665 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝑋 = ∪ 𝐽) |
13 | 12 | pweqd 4113 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝒫 𝑋 = 𝒫 ∪
𝐽) |
14 | 7, 13 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝒫 𝑋) |
15 | 2, 14 | unssd 3751 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋) |
16 | | ssun1 3738 |
. . . . . . . 8
⊢ 𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) |
17 | | filn0 21476 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) |
18 | | ssn0 3928 |
. . . . . . . 8
⊢ ((𝐹 ⊆ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∧ 𝐹 ≠ ∅) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅) |
19 | 16, 17, 18 | sylancr 694 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅) |
20 | 19 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅) |
21 | | incom 3767 |
. . . . . . . . . . . 12
⊢ (𝑦 ∩ 𝑥) = (𝑥 ∩ 𝑦) |
22 | | fclsneii 21631 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥 ∈ 𝐹) → (𝑦 ∩ 𝑥) ≠ ∅) |
23 | 21, 22 | syl5eqner 2857 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∩ 𝑦) ≠ ∅) |
24 | 23 | 3com23 1263 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑥 ∩ 𝑦) ≠ ∅) |
25 | 24 | 3expb 1258 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑦) ≠ ∅) |
26 | 25 | adantll 746 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ ((nei‘𝐽)‘{𝐴}))) → (𝑥 ∩ 𝑦) ≠ ∅) |
27 | 26 | ralrimivva 2954 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥 ∩ 𝑦) ≠ ∅) |
28 | | filfbas 21462 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
29 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ∈ (fBas‘𝑋)) |
30 | | istopon 20540 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽)) |
31 | 4, 12, 30 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐽 ∈ (TopOn‘𝑋)) |
32 | 5 | fclselbas 21630 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ ∪ 𝐽) |
33 | 32 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ ∪ 𝐽) |
34 | 33, 12 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ 𝑋) |
35 | 34 | snssd 4281 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ⊆ 𝑋) |
36 | | snnzg 4251 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → {𝐴} ≠ ∅) |
37 | 36 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → {𝐴} ≠ ∅) |
38 | | neifil 21494 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝐴} ⊆ 𝑋 ∧ {𝐴} ≠ ∅) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋)) |
39 | 31, 35, 37, 38 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋)) |
40 | | filfbas 21462 |
. . . . . . . . 9
⊢
(((nei‘𝐽)‘{𝐴}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) |
42 | | fbunfip 21483 |
. . . . . . . 8
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ (fBas‘𝑋)) → (¬ ∅ ∈
(fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥 ∩ 𝑦) ≠ ∅)) |
43 | 29, 41, 42 | syl2anc 691 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (¬ ∅ ∈
(fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴}))) ↔ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ ((nei‘𝐽)‘{𝐴})(𝑥 ∩ 𝑦) ≠ ∅)) |
44 | 27, 43 | mpbird 246 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ¬ ∅ ∈
(fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴})))) |
45 | | filtop 21469 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
46 | | fsubbas 21481 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐹 → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴})))))) |
47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴})))))) |
48 | 47 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) ↔ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ 𝒫 𝑋 ∧ (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴})))))) |
49 | 15, 20, 44, 48 | mpbir3and 1238 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋)) |
50 | | fgcl 21492 |
. . . . 5
⊢
((fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋)) |
51 | 49, 50 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋)) |
52 | | fvex 6113 |
. . . . . . . . 9
⊢
((nei‘𝐽)‘{𝐴}) ∈ V |
53 | | unexg 6857 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ((nei‘𝐽)‘{𝐴}) ∈ V) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V) |
54 | 52, 53 | mpan2 703 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V) |
55 | | ssfii 8208 |
. . . . . . . 8
⊢ ((𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ∈ V → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) |
56 | 54, 55 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) |
57 | 56 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐹 ∪ ((nei‘𝐽)‘{𝐴})) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) |
58 | 57 | unssad 3752 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) |
59 | | ssfg 21486 |
. . . . . 6
⊢
((fi‘(𝐹 ∪
((nei‘𝐽)‘{𝐴}))) ∈ (fBas‘𝑋) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) |
60 | 49, 59 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) |
61 | 58, 60 | sstrd 3578 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) |
62 | 57 | unssbd 3753 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) |
63 | 62, 60 | sstrd 3578 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) |
64 | | elflim 21585 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) |
65 | 31, 51, 64 | syl2anc 691 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → (𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) |
66 | 34, 63, 65 | mpbir2and 959 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))) |
67 | | sseq2 3590 |
. . . . . 6
⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐹 ⊆ 𝑔 ↔ 𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))) |
68 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐽 fLim 𝑔) = (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))) |
69 | 68 | eleq2d 2673 |
. . . . . 6
⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → (𝐴 ∈ (𝐽 fLim 𝑔) ↔ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) |
70 | 67, 69 | anbi12d 743 |
. . . . 5
⊢ (𝑔 = (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) → ((𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)) ↔ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))))))) |
71 | 70 | rspcev 3282 |
. . . 4
⊢ (((𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴})))) ∧ 𝐴 ∈ (𝐽 fLim (𝑋filGen(fi‘(𝐹 ∪ ((nei‘𝐽)‘{𝐴}))))))) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) |
72 | 51, 61, 66, 71 | syl12anc 1316 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fClus 𝐹)) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) |
73 | 72 | ex 449 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) → ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) |
74 | | simprl 790 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝑔 ∈ (Fil‘𝑋)) |
75 | | simprrr 801 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fLim 𝑔)) |
76 | | flimtopon 21584 |
. . . . . . 7
⊢ (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋))) |
77 | 75, 76 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝑔 ∈ (Fil‘𝑋))) |
78 | 74, 77 | mpbird 246 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐽 ∈ (TopOn‘𝑋)) |
79 | | simpl 472 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹 ∈ (Fil‘𝑋)) |
80 | | simprrl 800 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐹 ⊆ 𝑔) |
81 | | fclsss2 21637 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝑔) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹)) |
82 | 78, 79, 80, 81 | syl3anc 1318 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → (𝐽 fClus 𝑔) ⊆ (𝐽 fClus 𝐹)) |
83 | | flimfcls 21640 |
. . . . 5
⊢ (𝐽 fLim 𝑔) ⊆ (𝐽 fClus 𝑔) |
84 | 83, 75 | sseldi 3566 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝑔)) |
85 | 82, 84 | sseldd 3569 |
. . 3
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ (𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) → 𝐴 ∈ (𝐽 fClus 𝐹)) |
86 | 85 | rexlimdvaa 3014 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → (∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)) → 𝐴 ∈ (𝐽 fClus 𝐹))) |
87 | 73, 86 | impbid 201 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) |