Step | Hyp | Ref
| Expression |
1 | | cmptop 21008 |
. . . 4
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
2 | | flimfnfcls.x |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
3 | 2 | fclsval 21622 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐽 fClus 𝐹) = if(𝑋 = 𝑋, ∩ 𝑥 ∈ 𝐹 ((cls‘𝐽)‘𝑥), ∅)) |
4 | | eqid 2610 |
. . . . . 6
⊢ 𝑋 = 𝑋 |
5 | 4 | iftruei 4043 |
. . . . 5
⊢ if(𝑋 = 𝑋, ∩ 𝑥 ∈ 𝐹 ((cls‘𝐽)‘𝑥), ∅) = ∩ 𝑥 ∈ 𝐹 ((cls‘𝐽)‘𝑥) |
6 | 3, 5 | syl6eq 2660 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐽 fClus 𝐹) = ∩
𝑥 ∈ 𝐹 ((cls‘𝐽)‘𝑥)) |
7 | 1, 6 | sylan 487 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐽 fClus 𝐹) = ∩
𝑥 ∈ 𝐹 ((cls‘𝐽)‘𝑥)) |
8 | | fvex 6113 |
. . . 4
⊢
((cls‘𝐽)‘𝑥) ∈ V |
9 | 8 | dfiin3 5302 |
. . 3
⊢ ∩ 𝑥 ∈ 𝐹 ((cls‘𝐽)‘𝑥) = ∩ ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) |
10 | 7, 9 | syl6eq 2660 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐽 fClus 𝐹) = ∩ ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥))) |
11 | | simpl 472 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → 𝐽 ∈ Comp) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝐽 ∈ Comp) |
13 | 12, 1 | syl 17 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝐽 ∈ Top) |
14 | | filelss 21466 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹) → 𝑥 ⊆ 𝑋) |
15 | 14 | adantll 746 |
. . . . . 6
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ⊆ 𝑋) |
16 | 2 | clscld 20661 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋) → ((cls‘𝐽)‘𝑥) ∈ (Clsd‘𝐽)) |
17 | 13, 15, 16 | syl2anc 691 |
. . . . 5
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → ((cls‘𝐽)‘𝑥) ∈ (Clsd‘𝐽)) |
18 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) = (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) |
19 | 17, 18 | fmptd 6292 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)):𝐹⟶(Clsd‘𝐽)) |
20 | | frn 5966 |
. . . 4
⊢ ((𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)):𝐹⟶(Clsd‘𝐽) → ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ⊆ (Clsd‘𝐽)) |
21 | 19, 20 | syl 17 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ⊆ (Clsd‘𝐽)) |
22 | | simpr 476 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → 𝐹 ∈ (Fil‘𝑋)) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋)) |
24 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ 𝐹) |
25 | 2 | clsss3 20673 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋) → ((cls‘𝐽)‘𝑥) ⊆ 𝑋) |
26 | 13, 15, 25 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → ((cls‘𝐽)‘𝑥) ⊆ 𝑋) |
27 | 2 | sscls 20670 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ ((cls‘𝐽)‘𝑥)) |
28 | 13, 15, 27 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ⊆ ((cls‘𝐽)‘𝑥)) |
29 | | filss 21467 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ∈ 𝐹 ∧ ((cls‘𝐽)‘𝑥) ⊆ 𝑋 ∧ 𝑥 ⊆ ((cls‘𝐽)‘𝑥))) → ((cls‘𝐽)‘𝑥) ∈ 𝐹) |
30 | 23, 24, 26, 28, 29 | syl13anc 1320 |
. . . . . . . 8
⊢ (((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ 𝐹) → ((cls‘𝐽)‘𝑥) ∈ 𝐹) |
31 | 30, 18 | fmptd 6292 |
. . . . . . 7
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)):𝐹⟶𝐹) |
32 | | frn 5966 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)):𝐹⟶𝐹 → ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ⊆ 𝐹) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ⊆ 𝐹) |
34 | | fiss 8213 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ⊆ 𝐹) → (fi‘ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥))) ⊆ (fi‘𝐹)) |
35 | 22, 33, 34 | syl2anc 691 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (fi‘ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥))) ⊆ (fi‘𝐹)) |
36 | | filfi 21473 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹) |
37 | 22, 36 | syl 17 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (fi‘𝐹) = 𝐹) |
38 | 35, 37 | sseqtrd 3604 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (fi‘ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥))) ⊆ 𝐹) |
39 | | 0nelfil 21463 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝐹) |
40 | 22, 39 | syl 17 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → ¬ ∅ ∈
𝐹) |
41 | 38, 40 | ssneldd 3571 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → ¬ ∅ ∈
(fi‘ran (𝑥 ∈
𝐹 ↦ ((cls‘𝐽)‘𝑥)))) |
42 | | cmpfii 21022 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ⊆ (Clsd‘𝐽) ∧ ¬ ∅ ∈ (fi‘ran
(𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)))) → ∩ ran
(𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ≠ ∅) |
43 | 11, 21, 41, 42 | syl3anc 1318 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → ∩ ran (𝑥 ∈ 𝐹 ↦ ((cls‘𝐽)‘𝑥)) ≠ ∅) |
44 | 10, 43 | eqnetrd 2849 |
1
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐽 fClus 𝐹) ≠ ∅) |