| Step | Hyp | Ref
| Expression |
| 1 | | minvec.p |
. 2
⊢ 𝑃 = ∪
(𝐽 fLim (𝑋filGen𝐹)) |
| 2 | | ovex 7464 |
. . . . 5
⊢ (𝐽 fLim (𝑋filGen𝐹)) ∈ V |
| 3 | 2 | uniex 7761 |
. . . 4
⊢ ∪ (𝐽
fLim (𝑋filGen𝐹)) ∈ V |
| 4 | 3 | snid 4662 |
. . 3
⊢ ∪ (𝐽
fLim (𝑋filGen𝐹)) ∈ {∪ (𝐽
fLim (𝑋filGen𝐹))} |
| 5 | | minvec.u |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ ℂPreHil) |
| 6 | | cphngp 25207 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ ℂPreHil →
𝑈 ∈
NrmGrp) |
| 7 | | ngpxms 24614 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈
∞MetSp) |
| 8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ ∞MetSp) |
| 9 | | minvec.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (TopOpen‘𝑈) |
| 10 | | minvec.x |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝑈) |
| 11 | | minvec.d |
. . . . . . . . . . . 12
⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋)) |
| 12 | 9, 10, 11 | xmstopn 24461 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ∞MetSp →
𝐽 = (MetOpen‘𝐷)) |
| 13 | 8, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷)) |
| 14 | 13 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 ↾t 𝑌) = ((MetOpen‘𝐷) ↾t 𝑌)) |
| 15 | 10, 11 | xmsxmet 24466 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ∞MetSp →
𝐷 ∈
(∞Met‘𝑋)) |
| 16 | 8, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 17 | | minvec.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈)) |
| 18 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
| 19 | 10, 18 | lssss 20934 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋) |
| 20 | 17, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
| 21 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌)) |
| 22 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
| 23 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(MetOpen‘(𝐷
↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) |
| 24 | 21, 22, 23 | metrest 24537 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((MetOpen‘𝐷) ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
| 25 | 16, 20, 24 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((MetOpen‘𝐷) ↾t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))) |
| 26 | 14, 25 | eqtr2d 2778 |
. . . . . . . 8
⊢ (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (𝐽 ↾t 𝑌)) |
| 27 | | minvec.m |
. . . . . . . . . . . 12
⊢ − =
(-g‘𝑈) |
| 28 | | minvec.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (norm‘𝑈) |
| 29 | | minvec.w |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp) |
| 30 | | minvec.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 31 | | minvec.r |
. . . . . . . . . . . 12
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦))) |
| 32 | | minvec.s |
. . . . . . . . . . . 12
⊢ 𝑆 = inf(𝑅, ℝ, < ) |
| 33 | | minvec.f |
. . . . . . . . . . . 12
⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)}) |
| 34 | 10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33 | minveclem3b 25462 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌)) |
| 35 | | fgcl 23886 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌)) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (Fil‘𝑌)) |
| 37 | 10 | fvexi 6920 |
. . . . . . . . . . 11
⊢ 𝑋 ∈ V |
| 38 | 37 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ V) |
| 39 | | trfg 23899 |
. . . . . . . . . 10
⊢ (((𝑌filGen𝐹) ∈ (Fil‘𝑌) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V) → ((𝑋filGen(𝑌filGen𝐹)) ↾t 𝑌) = (𝑌filGen𝐹)) |
| 40 | 36, 20, 38, 39 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾t 𝑌) = (𝑌filGen𝐹)) |
| 41 | | fgabs 23887 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)) |
| 42 | 34, 20, 41 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾t 𝑌) = ((𝑋filGen𝐹) ↾t 𝑌)) |
| 44 | 40, 43 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → (𝑌filGen𝐹) = ((𝑋filGen𝐹) ↾t 𝑌)) |
| 45 | 26, 44 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝐹) ↾t 𝑌))) |
| 46 | | xmstps 24463 |
. . . . . . . . . 10
⊢ (𝑈 ∈ ∞MetSp →
𝑈 ∈
TopSp) |
| 47 | 8, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ TopSp) |
| 48 | 10, 9 | istps 22940 |
. . . . . . . . 9
⊢ (𝑈 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋)) |
| 49 | 47, 48 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 50 | | fbsspw 23840 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌) |
| 51 | 34, 50 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌) |
| 52 | 20 | sspwd 4613 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋) |
| 53 | 51, 52 | sstrd 3994 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋) |
| 54 | | fbasweak 23873 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋)) |
| 55 | 34, 53, 38, 54 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋)) |
| 56 | | fgcl 23886 |
. . . . . . . . 9
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
| 57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |
| 58 | | filfbas 23856 |
. . . . . . . . . . . . 13
⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌)) |
| 59 | 34, 35, 58 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑌)) |
| 60 | | fbsspw 23840 |
. . . . . . . . . . . . . 14
⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌) |
| 61 | 59, 60 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑌) |
| 62 | 61, 52 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑋) |
| 63 | | fbasweak 23873 |
. . . . . . . . . . . 12
⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋)) |
| 64 | 59, 62, 38, 63 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑋)) |
| 65 | | ssfg 23880 |
. . . . . . . . . . 11
⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹))) |
| 66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹))) |
| 67 | 66, 42 | sseqtrd 4020 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen𝐹)) |
| 68 | | filtop 23863 |
. . . . . . . . . 10
⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐹)) |
| 69 | 36, 68 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐹)) |
| 70 | 67, 69 | sseldd 3984 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑋filGen𝐹)) |
| 71 | | flimrest 23991 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ 𝑌 ∈ (𝑋filGen𝐹)) → ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝐹) ↾t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
| 72 | 49, 57, 70, 71 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → ((𝐽 ↾t 𝑌) fLim ((𝑋filGen𝐹) ↾t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
| 73 | 45, 72 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
| 74 | 10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11 | minveclem3a 25461 |
. . . . . . 7
⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) |
| 75 | 10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33 | minveclem3 25463 |
. . . . . . 7
⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) |
| 76 | 23 | cmetcvg 25319 |
. . . . . . 7
⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ∧ (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅) |
| 77 | 74, 75, 76 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅) |
| 78 | 73, 77 | eqnetrrd 3009 |
. . . . 5
⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) |
| 79 | 78 | neneqd 2945 |
. . . 4
⊢ (𝜑 → ¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅) |
| 80 | | inss1 4237 |
. . . . . . 7
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) |
| 81 | 22 | methaus 24533 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ (∞Met‘𝑋) → (MetOpen‘𝐷) ∈ Haus) |
| 82 | 15, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ ∞MetSp →
(MetOpen‘𝐷) ∈
Haus) |
| 83 | 12, 82 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ∞MetSp →
𝐽 ∈
Haus) |
| 84 | | hausflimi 23988 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ Haus →
∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
| 85 | 8, 83, 84 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
| 86 | | ssn0 4404 |
. . . . . . . . . . . 12
⊢ ((((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) ∧ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅) |
| 87 | 80, 78, 86 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅) |
| 88 | | n0moeu 4359 |
. . . . . . . . . . 11
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≠ ∅ → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))) |
| 89 | 87, 88 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))) |
| 90 | 85, 89 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
| 91 | | euen1b 9068 |
. . . . . . . . 9
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1o ↔
∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))) |
| 92 | 90, 91 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≈ 1o) |
| 93 | | en1b 9065 |
. . . . . . . 8
⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1o ↔ (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))}) |
| 94 | 92, 93 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))}) |
| 95 | 80, 94 | sseqtrid 4026 |
. . . . . 6
⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪
(𝐽 fLim (𝑋filGen𝐹))}) |
| 96 | | sssn 4826 |
. . . . . 6
⊢ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪
(𝐽 fLim (𝑋filGen𝐹))} ↔ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})) |
| 97 | 95, 96 | sylib 218 |
. . . . 5
⊢ (𝜑 → (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})) |
| 98 | 97 | ord 865 |
. . . 4
⊢ (𝜑 → (¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})) |
| 99 | 79, 98 | mpd 15 |
. . 3
⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}) |
| 100 | 4, 99 | eleqtrrid 2848 |
. 2
⊢ (𝜑 → ∪ (𝐽
fLim (𝑋filGen𝐹)) ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |
| 101 | 1, 100 | eqeltrid 2845 |
1
⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌)) |