Step | Hyp | Ref
| Expression |
1 | | cmetmet 23084 |
. . . . 5
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
2 | | metxmet 22139 |
. . . . 5
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
4 | | bcth.2 |
. . . . . . . . . 10
⊢ 𝐽 = (MetOpen‘𝐷) |
5 | 4 | mopntop 22245 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
6 | 5 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → 𝐽 ∈ Top) |
7 | | ffvelrn 6357 |
. . . . . . . . . 10
⊢ ((𝑀:ℕ⟶𝐽 ∧ 𝑘 ∈ ℕ) → (𝑀‘𝑘) ∈ 𝐽) |
8 | | elssuni 4467 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑘) ∈ 𝐽 → (𝑀‘𝑘) ⊆ ∪ 𝐽) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀:ℕ⟶𝐽 ∧ 𝑘 ∈ ℕ) → (𝑀‘𝑘) ⊆ ∪ 𝐽) |
10 | 9 | adantll 750 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → (𝑀‘𝑘) ⊆ ∪ 𝐽) |
11 | | eqid 2622 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
12 | 11 | clsval2 20854 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝑀‘𝑘) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝑀‘𝑘)) = (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽
∖ (𝑀‘𝑘))))) |
13 | 6, 10, 12 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((cls‘𝐽)‘(𝑀‘𝑘)) = (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽
∖ (𝑀‘𝑘))))) |
14 | 4 | mopnuni 22246 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
15 | 14 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → 𝑋 = ∪ 𝐽) |
16 | 13, 15 | eqeq12d 2637 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → (((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋 ↔ (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽
∖ (𝑀‘𝑘)))) = ∪ 𝐽)) |
17 | | difeq2 3722 |
. . . . . . . 8
⊢ ((∪ 𝐽
∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘)))) = ∪ 𝐽 → (∪ 𝐽
∖ (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))))) = (∪ 𝐽 ∖ ∪ 𝐽)) |
18 | | difid 3948 |
. . . . . . . 8
⊢ (∪ 𝐽
∖ ∪ 𝐽) = ∅ |
19 | 17, 18 | syl6eq 2672 |
. . . . . . 7
⊢ ((∪ 𝐽
∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘)))) = ∪ 𝐽 → (∪ 𝐽
∖ (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))))) = ∅) |
20 | | difss 3737 |
. . . . . . . . . . . 12
⊢ (∪ 𝐽
∖ (𝑀‘𝑘)) ⊆ ∪ 𝐽 |
21 | 11 | ntropn 20853 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ (∪ 𝐽
∖ (𝑀‘𝑘)) ⊆ ∪ 𝐽)
→ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))) ∈ 𝐽) |
22 | 6, 20, 21 | sylancl 694 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((int‘𝐽)‘(∪ 𝐽
∖ (𝑀‘𝑘))) ∈ 𝐽) |
23 | | elssuni 4467 |
. . . . . . . . . . 11
⊢
(((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))) ∈ 𝐽 → ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))) ⊆ ∪
𝐽) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((int‘𝐽)‘(∪ 𝐽
∖ (𝑀‘𝑘))) ⊆ ∪ 𝐽) |
25 | | dfss4 3858 |
. . . . . . . . . 10
⊢
(((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))) ⊆ ∪
𝐽 ↔ (∪ 𝐽
∖ (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))))) = ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘)))) |
26 | 24, 25 | sylib 208 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → (∪ 𝐽
∖ (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))))) = ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘)))) |
27 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ) |
28 | | elfvdm 6220 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met) |
29 | | difexg 4808 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ dom ∞Met →
(𝑋 ∖ (𝑀‘𝑘)) ∈ V) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∖ (𝑀‘𝑘)) ∈ V) |
31 | 30 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (𝑋 ∖ (𝑀‘𝑘)) ∈ V) |
32 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → (𝑀‘𝑥) = (𝑀‘𝑘)) |
33 | 32 | difeq2d 3728 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (𝑋 ∖ (𝑀‘𝑥)) = (𝑋 ∖ (𝑀‘𝑘))) |
34 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))) = (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))) |
35 | 33, 34 | fvmptg 6280 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℕ ∧ (𝑋 ∖ (𝑀‘𝑘)) ∈ V) → ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘) = (𝑋 ∖ (𝑀‘𝑘))) |
36 | 27, 31, 35 | syl2anr 495 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘) = (𝑋 ∖ (𝑀‘𝑘))) |
37 | 15 | difeq1d 3727 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → (𝑋 ∖ (𝑀‘𝑘)) = (∪ 𝐽 ∖ (𝑀‘𝑘))) |
38 | 36, 37 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘) = (∪ 𝐽 ∖ (𝑀‘𝑘))) |
39 | 38 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘)))) |
40 | 26, 39 | eqtr4d 2659 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → (∪ 𝐽
∖ (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))))) = ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘))) |
41 | 40 | eqeq1d 2624 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((∪ 𝐽
∖ (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘))))) = ∅ ↔ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅)) |
42 | 19, 41 | syl5ib 234 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ((∪ 𝐽
∖ ((int‘𝐽)‘(∪ 𝐽 ∖ (𝑀‘𝑘)))) = ∪ 𝐽 → ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅)) |
43 | 16, 42 | sylbid 230 |
. . . . 5
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → (((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋 → ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅)) |
44 | 43 | ralimdva 2962 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (∀𝑘 ∈ ℕ ((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅)) |
45 | 3, 44 | sylan 488 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (∀𝑘 ∈ ℕ ((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅)) |
46 | | ffvelrn 6357 |
. . . . . . . . 9
⊢ ((𝑀:ℕ⟶𝐽 ∧ 𝑥 ∈ ℕ) → (𝑀‘𝑥) ∈ 𝐽) |
47 | 14 | difeq1d 3727 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∖ (𝑀‘𝑥)) = (∪ 𝐽 ∖ (𝑀‘𝑥))) |
48 | 47 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑀‘𝑥) ∈ 𝐽) → (𝑋 ∖ (𝑀‘𝑥)) = (∪ 𝐽 ∖ (𝑀‘𝑥))) |
49 | 11 | opncld 20837 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ Top ∧ (𝑀‘𝑥) ∈ 𝐽) → (∪ 𝐽 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽)) |
50 | 5, 49 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑀‘𝑥) ∈ 𝐽) → (∪ 𝐽 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽)) |
51 | 48, 50 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑀‘𝑥) ∈ 𝐽) → (𝑋 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽)) |
52 | 46, 51 | sylan2 491 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑀:ℕ⟶𝐽 ∧ 𝑥 ∈ ℕ)) → (𝑋 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽)) |
53 | 52 | anassrs 680 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑥 ∈ ℕ) → (𝑋 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽)) |
54 | 53 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∀𝑥 ∈ ℕ (𝑋 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽)) |
55 | 3, 54 | sylan 488 |
. . . . 5
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∀𝑥 ∈ ℕ (𝑋 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽)) |
56 | 34 | fmpt 6381 |
. . . . 5
⊢
(∀𝑥 ∈
ℕ (𝑋 ∖ (𝑀‘𝑥)) ∈ (Clsd‘𝐽) ↔ (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))):ℕ⟶(Clsd‘𝐽)) |
57 | 55, 56 | sylib 208 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))):ℕ⟶(Clsd‘𝐽)) |
58 | | nne 2798 |
. . . . . . 7
⊢ (¬
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅ ↔ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅) |
59 | 58 | ralbii 2980 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ ¬ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅ ↔ ∀𝑘 ∈ ℕ
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅) |
60 | | ralnex 2992 |
. . . . . 6
⊢
(∀𝑘 ∈
ℕ ¬ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅ ↔ ¬ ∃𝑘 ∈ ℕ
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅) |
61 | 59, 60 | bitr3i 266 |
. . . . 5
⊢
(∀𝑘 ∈
ℕ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅ ↔ ¬ ∃𝑘 ∈ ℕ
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅) |
62 | 4 | bcth 23126 |
. . . . . . 7
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))):ℕ⟶(Clsd‘𝐽) ∧ ((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))) ≠ ∅) → ∃𝑘 ∈ ℕ
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅) |
63 | 62 | 3expia 1267 |
. . . . . 6
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))):ℕ⟶(Clsd‘𝐽)) → (((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))) ≠ ∅ → ∃𝑘 ∈ ℕ
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅)) |
64 | 63 | necon1bd 2812 |
. . . . 5
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))):ℕ⟶(Clsd‘𝐽)) → (¬ ∃𝑘 ∈ ℕ
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) ≠ ∅ → ((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))) = ∅)) |
65 | 61, 64 | syl5bi 232 |
. . . 4
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))):ℕ⟶(Clsd‘𝐽)) → (∀𝑘 ∈ ℕ
((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅ → ((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))) = ∅)) |
66 | 57, 65 | syldan 487 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (∀𝑘 ∈ ℕ ((int‘𝐽)‘((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘)) = ∅ → ((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))) = ∅)) |
67 | | difeq2 3722 |
. . . . 5
⊢
(((int‘𝐽)‘∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥)))) = ∅ → (∪ 𝐽
∖ ((int‘𝐽)‘∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥))))) = (∪ 𝐽 ∖
∅)) |
68 | | difexg 4808 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ dom ∞Met →
(𝑋 ∖ (𝑀‘𝑥)) ∈ V) |
69 | 28, 68 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 ∖ (𝑀‘𝑥)) ∈ V) |
70 | 69 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑥 ∈ ℕ) → (𝑋 ∖ (𝑀‘𝑥)) ∈ V) |
71 | 70 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∀𝑥 ∈ ℕ (𝑋 ∖ (𝑀‘𝑥)) ∈ V) |
72 | 34 | fnmpt 6020 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
ℕ (𝑋 ∖ (𝑀‘𝑥)) ∈ V → (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))) Fn ℕ) |
73 | | fniunfv 6505 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))) Fn ℕ → ∪ 𝑘 ∈ ℕ ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘) = ∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))) |
74 | 71, 72, 73 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∪
𝑘 ∈ ℕ ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘) = ∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))) |
75 | 36 | iuneq2dv 4542 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∪
𝑘 ∈ ℕ ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘) = ∪ 𝑘 ∈ ℕ (𝑋 ∖ (𝑀‘𝑘))) |
76 | 33 | cbviunv 4559 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ ℕ (𝑋 ∖ (𝑀‘𝑥)) = ∪
𝑘 ∈ ℕ (𝑋 ∖ (𝑀‘𝑘)) |
77 | 75, 76 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∪
𝑘 ∈ ℕ ((𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥)))‘𝑘) = ∪ 𝑥 ∈ ℕ (𝑋 ∖ (𝑀‘𝑥))) |
78 | 74, 77 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥))) = ∪
𝑥 ∈ ℕ (𝑋 ∖ (𝑀‘𝑥))) |
79 | | iundif2 4587 |
. . . . . . . . . . 11
⊢ ∪ 𝑥 ∈ ℕ (𝑋 ∖ (𝑀‘𝑥)) = (𝑋 ∖ ∩
𝑥 ∈ ℕ (𝑀‘𝑥)) |
80 | 78, 79 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥))) = (𝑋 ∖ ∩
𝑥 ∈ ℕ (𝑀‘𝑥))) |
81 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝑀:ℕ⟶𝐽 → 𝑀 Fn ℕ) |
82 | 81 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → 𝑀 Fn ℕ) |
83 | | fniinfv 6257 |
. . . . . . . . . . . 12
⊢ (𝑀 Fn ℕ → ∩ 𝑥 ∈ ℕ (𝑀‘𝑥) = ∩ ran 𝑀) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∩
𝑥 ∈ ℕ (𝑀‘𝑥) = ∩ ran 𝑀) |
85 | 84 | difeq2d 3728 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (𝑋 ∖ ∩
𝑥 ∈ ℕ (𝑀‘𝑥)) = (𝑋 ∖ ∩ ran
𝑀)) |
86 | 14 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → 𝑋 = ∪ 𝐽) |
87 | 86 | difeq1d 3727 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (𝑋 ∖ ∩ ran
𝑀) = (∪ 𝐽
∖ ∩ ran 𝑀)) |
88 | 80, 85, 87 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥))) = (∪ 𝐽 ∖ ∩ ran 𝑀)) |
89 | 88 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ((int‘𝐽)‘∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥)))) = ((int‘𝐽)‘(∪ 𝐽 ∖ ∩ ran 𝑀))) |
90 | 89 | difeq2d 3728 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (∪ 𝐽 ∖ ((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))))) = (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽
∖ ∩ ran 𝑀)))) |
91 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → 𝐽 ∈ Top) |
92 | | 1nn 11031 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
93 | | biidd 252 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∩ ran
𝑀 ⊆ ∪ 𝐽)
↔ ((𝐷 ∈
(∞Met‘𝑋) ∧
𝑀:ℕ⟶𝐽) → ∩ ran 𝑀 ⊆ ∪ 𝐽))) |
94 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑀‘𝑘) ∈ ran 𝑀) |
95 | 82, 94 | sylan 488 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → (𝑀‘𝑘) ∈ ran 𝑀) |
96 | | intss1 4492 |
. . . . . . . . . . . . 13
⊢ ((𝑀‘𝑘) ∈ ran 𝑀 → ∩ ran
𝑀 ⊆ (𝑀‘𝑘)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ∩ ran 𝑀 ⊆ (𝑀‘𝑘)) |
98 | 97, 10 | sstrd 3613 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) ∧ 𝑘 ∈ ℕ) → ∩ ran 𝑀 ⊆ ∪ 𝐽) |
99 | 98 | expcom 451 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∩ ran
𝑀 ⊆ ∪ 𝐽)) |
100 | 93, 99 | vtoclga 3272 |
. . . . . . . . 9
⊢ (1 ∈
ℕ → ((𝐷 ∈
(∞Met‘𝑋) ∧
𝑀:ℕ⟶𝐽) → ∩ ran 𝑀 ⊆ ∪ 𝐽)) |
101 | 92, 100 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ∩ ran
𝑀 ⊆ ∪ 𝐽) |
102 | 11 | clsval2 20854 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ ∩ ran 𝑀 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘∩ ran 𝑀) = (∪ 𝐽 ∖ ((int‘𝐽)‘(∪ 𝐽
∖ ∩ ran 𝑀)))) |
103 | 91, 101, 102 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ((cls‘𝐽)‘∩ ran
𝑀) = (∪ 𝐽
∖ ((int‘𝐽)‘(∪ 𝐽 ∖ ∩ ran 𝑀)))) |
104 | 90, 103 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (∪ 𝐽 ∖ ((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))))) = ((cls‘𝐽)‘∩ ran
𝑀)) |
105 | | dif0 3950 |
. . . . . . 7
⊢ (∪ 𝐽
∖ ∅) = ∪ 𝐽 |
106 | 86, 105 | syl6reqr 2675 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (∪ 𝐽 ∖ ∅) = 𝑋) |
107 | 104, 106 | eqeq12d 2637 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → ((∪
𝐽 ∖ ((int‘𝐽)‘∪ ran (𝑥 ∈ ℕ ↦ (𝑋 ∖ (𝑀‘𝑥))))) = (∪ 𝐽 ∖ ∅) ↔
((cls‘𝐽)‘∩ ran 𝑀) = 𝑋)) |
108 | 67, 107 | syl5ib 234 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (((int‘𝐽)‘∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥)))) = ∅ → ((cls‘𝐽)‘∩ ran 𝑀) = 𝑋)) |
109 | 3, 108 | sylan 488 |
. . 3
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (((int‘𝐽)‘∪ ran
(𝑥 ∈ ℕ ↦
(𝑋 ∖ (𝑀‘𝑥)))) = ∅ → ((cls‘𝐽)‘∩ ran 𝑀) = 𝑋)) |
110 | 45, 66, 109 | 3syld 60 |
. 2
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽) → (∀𝑘 ∈ ℕ ((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋 → ((cls‘𝐽)‘∩ ran
𝑀) = 𝑋)) |
111 | 110 | 3impia 1261 |
1
⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ ((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋) → ((cls‘𝐽)‘∩ ran
𝑀) = 𝑋) |