Step | Hyp | Ref
| Expression |
1 | | cmetcau.3 |
. . . . . . . . 9
β’ (π β π· β (CMetβπ)) |
2 | | cmetmet 24666 |
. . . . . . . . 9
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
β’ (π β π· β (Metβπ)) |
4 | | metxmet 23703 |
. . . . . . . 8
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
5 | 3, 4 | syl 17 |
. . . . . . 7
β’ (π β π· β (βMetβπ)) |
6 | | cmetcau.1 |
. . . . . . . 8
β’ π½ = (MetOpenβπ·) |
7 | 6 | mopntopon 23808 |
. . . . . . 7
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
8 | 5, 7 | syl 17 |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
9 | | 1z 12540 |
. . . . . . . 8
β’ 1 β
β€ |
10 | | nnuz 12813 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
11 | 10 | uzfbas 23265 |
. . . . . . . 8
β’ (1 β
β€ β (β€β₯ β β) β
(fBasββ)) |
12 | 9, 11 | mp1i 13 |
. . . . . . 7
β’ (π β (β€β₯
β β) β (fBasββ)) |
13 | | fgcl 23245 |
. . . . . . 7
β’
((β€β₯ β β) β (fBasββ)
β (βfilGen(β€β₯ β β)) β
(Filββ)) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π β
(βfilGen(β€β₯ β β)) β
(Filββ)) |
15 | | elfvdm 6884 |
. . . . . . . . . . . 12
β’ (π· β (CMetβπ) β π β dom CMet) |
16 | 1, 15 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β dom CMet) |
17 | | cnex 11139 |
. . . . . . . . . . . 12
β’ β
β V |
18 | 17 | a1i 11 |
. . . . . . . . . . 11
β’ (π β β β
V) |
19 | | cmetcau.5 |
. . . . . . . . . . . 12
β’ (π β πΉ β (Cauβπ·)) |
20 | | caufpm 24662 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β πΉ β (π βpm
β)) |
21 | 5, 19, 20 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β πΉ β (π βpm
β)) |
22 | | elpm2g 8789 |
. . . . . . . . . . . 12
β’ ((π β dom CMet β§ β
β V) β (πΉ β
(π βpm
β) β (πΉ:dom
πΉβΆπ β§ dom πΉ β β))) |
23 | 22 | simprbda 500 |
. . . . . . . . . . 11
β’ (((π β dom CMet β§ β
β V) β§ πΉ β
(π βpm
β)) β πΉ:dom
πΉβΆπ) |
24 | 16, 18, 21, 23 | syl21anc 837 |
. . . . . . . . . 10
β’ (π β πΉ:dom πΉβΆπ) |
25 | 24 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β πΉ:dom πΉβΆπ) |
26 | 25 | ffvelcdmda 7040 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π₯ β dom πΉ) β (πΉβπ₯) β π) |
27 | | cmetcau.4 |
. . . . . . . . 9
β’ (π β π β π) |
28 | 27 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ Β¬ π₯ β dom πΉ) β π β π) |
29 | 26, 28 | ifclda 4526 |
. . . . . . 7
β’ ((π β§ π₯ β β) β if(π₯ β dom πΉ, (πΉβπ₯), π) β π) |
30 | | cmetcau.6 |
. . . . . . 7
β’ πΊ = (π₯ β β β¦ if(π₯ β dom πΉ, (πΉβπ₯), π)) |
31 | 29, 30 | fmptd 7067 |
. . . . . 6
β’ (π β πΊ:ββΆπ) |
32 | | flfval 23357 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§
(βfilGen(β€β₯ β β)) β
(Filββ) β§ πΊ:ββΆπ) β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)
= (π½ fLim ((π FilMap πΊ)β(βfilGen(β€β₯
β β))))) |
33 | 8, 14, 31, 32 | syl3anc 1372 |
. . . . 5
β’ (π β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)
= (π½ fLim ((π FilMap πΊ)β(βfilGen(β€β₯
β β))))) |
34 | | eqid 2737 |
. . . . . . . 8
β’
(βfilGen(β€β₯ β β)) =
(βfilGen(β€β₯ β β)) |
35 | 34 | fmfg 23316 |
. . . . . . 7
β’ ((π β dom CMet β§
(β€β₯ β β) β (fBasββ) β§
πΊ:ββΆπ) β ((π FilMap πΊ)β(β€β₯ β
β)) = ((π FilMap
πΊ)β(βfilGen(β€β₯
β β)))) |
36 | 16, 12, 31, 35 | syl3anc 1372 |
. . . . . 6
β’ (π β ((π FilMap πΊ)β(β€β₯ β
β)) = ((π FilMap
πΊ)β(βfilGen(β€β₯
β β)))) |
37 | 36 | oveq2d 7378 |
. . . . 5
β’ (π β (π½ fLim ((π FilMap πΊ)β(β€β₯ β
β))) = (π½ fLim
((π FilMap πΊ)β(βfilGen(β€β₯
β β))))) |
38 | 33, 37 | eqtr4d 2780 |
. . . 4
β’ (π β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)
= (π½ fLim ((π FilMap πΊ)β(β€β₯ β
β)))) |
39 | | biidd 262 |
. . . . . . . 8
β’ (π§ = 1 β (βπ β β βπ β
(β€β₯βπ)π β dom πΉ β βπ β β βπ β (β€β₯βπ)π β dom πΉ)) |
40 | | 1zzd 12541 |
. . . . . . . . . . . 12
β’ (π β 1 β
β€) |
41 | 10, 5, 40 | iscau3 24658 |
. . . . . . . . . . 11
β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ§ β
β+ βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ€ β (β€β₯βπ)((πΉβπ)π·(πΉβπ€)) < π§)))) |
42 | 41 | simplbda 501 |
. . . . . . . . . 10
β’ ((π β§ πΉ β (Cauβπ·)) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ€ β (β€β₯βπ)((πΉβπ)π·(πΉβπ€)) < π§)) |
43 | 19, 42 | mpdan 686 |
. . . . . . . . 9
β’ (π β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ€ β (β€β₯βπ)((πΉβπ)π·(πΉβπ€)) < π§)) |
44 | | simp1 1137 |
. . . . . . . . . . . 12
β’ ((π β dom πΉ β§ (πΉβπ) β π β§ βπ€ β (β€β₯βπ)((πΉβπ)π·(πΉβπ€)) < π§) β π β dom πΉ) |
45 | 44 | ralimi 3087 |
. . . . . . . . . . 11
β’
(βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ€ β (β€β₯βπ)((πΉβπ)π·(πΉβπ€)) < π§) β βπ β (β€β₯βπ)π β dom πΉ) |
46 | 45 | reximi 3088 |
. . . . . . . . . 10
β’
(βπ β
β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ€ β (β€β₯βπ)((πΉβπ)π·(πΉβπ€)) < π§) β βπ β β βπ β (β€β₯βπ)π β dom πΉ) |
47 | 46 | ralimi 3087 |
. . . . . . . . 9
β’
(βπ§ β
β+ βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ€ β (β€β₯βπ)((πΉβπ)π·(πΉβπ€)) < π§) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)π β dom πΉ) |
48 | 43, 47 | syl 17 |
. . . . . . . 8
β’ (π β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)π β dom πΉ) |
49 | | 1rp 12926 |
. . . . . . . . 9
β’ 1 β
β+ |
50 | 49 | a1i 11 |
. . . . . . . 8
β’ (π β 1 β
β+) |
51 | 39, 48, 50 | rspcdva 3585 |
. . . . . . 7
β’ (π β βπ β β βπ β (β€β₯βπ)π β dom πΉ) |
52 | | dfss3 3937 |
. . . . . . . . 9
β’
((β€β₯βπ) β dom πΉ β βπ β (β€β₯βπ)π β dom πΉ) |
53 | | nnsscn 12165 |
. . . . . . . . . . . . . 14
β’ β
β β |
54 | 31, 53 | jctir 522 |
. . . . . . . . . . . . 13
β’ (π β (πΊ:ββΆπ β§ β β
β)) |
55 | | elpm2r 8790 |
. . . . . . . . . . . . 13
β’ (((π β dom CMet β§ β
β V) β§ (πΊ:ββΆπ β§ β β β)) β
πΊ β (π βpm
β)) |
56 | 16, 18, 54, 55 | syl21anc 837 |
. . . . . . . . . . . 12
β’ (π β πΊ β (π βpm
β)) |
57 | 56 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β πΊ β (π βpm
β)) |
58 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(β€β₯βπ) = (β€β₯βπ) |
59 | 5 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β π· β (βMetβπ)) |
60 | | nnz 12527 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
61 | 60 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β π β β€) |
62 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β (πΉβπ) = (πΉβπ)) |
63 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β (πΉβπ) = (πΉβπ)) |
64 | 58, 59, 61, 62, 63 | iscau4 24659 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§
βπ§ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§)))) |
65 | 64 | simplbda 501 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ πΉ β (Cauβπ·)) β βπ§ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§)) |
66 | 19, 65 | mpidan 688 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β βπ§ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§)) |
67 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β π β β) |
68 | | eluznn 12850 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
69 | 67, 68 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β π β β) |
70 | | eluznn 12850 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
71 | 30, 29 | dmmptd 6651 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β dom πΊ = β) |
72 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β dom πΊ = β) |
73 | 72 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β (π β dom πΊ β π β β)) |
74 | 73 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β β) β π β dom πΊ) |
75 | 74 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β β) β (π β dom πΉ β π β dom πΊ)) |
76 | | idd 24 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β β) β ((πΉβπ) β π β (πΉβπ) β π)) |
77 | | idd 24 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β β) β (((πΉβπ)π·(πΉβπ)) < π§ β ((πΉβπ)π·(πΉβπ)) < π§)) |
78 | 75, 76, 77 | 3anim123d 1444 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β β) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§) β (π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§))) |
79 | 70, 78 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ (π β β β§ π β (β€β₯βπ))) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§) β (π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§))) |
80 | 79 | anassrs 469 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β β) β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§) β (π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§))) |
81 | 80 | ralimdva 3165 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β β) β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§) β βπ β (β€β₯βπ)(π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§))) |
82 | 69, 81 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§) β βπ β (β€β₯βπ)(π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§))) |
83 | 82 | reximdva 3166 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§))) |
84 | 83 | ralimdv 3167 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β (βπ§ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§) β βπ§ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§))) |
85 | 66, 84 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β βπ§ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§)) |
86 | | eluznn 12850 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
87 | 67, 86 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β π β β) |
88 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β
(β€β₯βπ) β dom πΉ) |
89 | 88 | sselda 3949 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β π β dom πΉ) |
90 | | iftrue 4497 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom πΉ β if(π β dom πΉ, (πΉβπ), π) = (πΉβπ)) |
91 | 90 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β dom πΉ) β if(π β dom πΉ, (πΉβπ), π) = (πΉβπ)) |
92 | | fvex 6860 |
. . . . . . . . . . . . . . . 16
β’ (πΉβπ) β V |
93 | 91, 92 | eqeltrdi 2846 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β dom πΉ) β if(π β dom πΉ, (πΉβπ), π) β V) |
94 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π₯ β dom πΉ β π β dom πΉ)) |
95 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
96 | 94, 95 | ifbieq1d 4515 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β if(π₯ β dom πΉ, (πΉβπ₯), π) = if(π β dom πΉ, (πΉβπ), π)) |
97 | 96, 30 | fvmptg 6951 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ if(π β dom πΉ, (πΉβπ), π) β V) β (πΊβπ) = if(π β dom πΉ, (πΉβπ), π)) |
98 | 93, 97 | syldan 592 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β dom πΉ) β (πΊβπ) = if(π β dom πΉ, (πΉβπ), π)) |
99 | 98, 91 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β dom πΉ) β (πΊβπ) = (πΉβπ)) |
100 | 87, 89, 99 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β (πΊβπ) = (πΉβπ)) |
101 | 88 | sselda 3949 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β π β dom πΉ) |
102 | 69, 101 | elind 4159 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β π β (β β© dom πΉ)) |
103 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΊβπ) = (πΊβπ)) |
104 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
105 | 103, 104 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΊβπ) = (πΉβπ) β (πΊβπ) = (πΉβπ))) |
106 | | elin 3931 |
. . . . . . . . . . . . . . 15
β’ (π β (β β© dom πΉ) β (π β β β§ π β dom πΉ)) |
107 | 106, 99 | sylbi 216 |
. . . . . . . . . . . . . 14
β’ (π β (β β© dom πΉ) β (πΊβπ) = (πΉβπ)) |
108 | 105, 107 | vtoclga 3537 |
. . . . . . . . . . . . 13
β’ (π β (β β© dom πΉ) β (πΊβπ) = (πΉβπ)) |
109 | 102, 108 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β§ π β (β€β₯βπ)) β (πΊβπ) = (πΉβπ)) |
110 | 58, 59, 61, 100, 109 | iscau4 24659 |
. . . . . . . . . . 11
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β (πΊ β (Cauβπ·) β (πΊ β (π βpm β) β§
βπ§ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)(π β dom πΊ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π§)))) |
111 | 57, 85, 110 | mpbir2and 712 |
. . . . . . . . . 10
β’ ((π β§ (π β β β§
(β€β₯βπ) β dom πΉ)) β πΊ β (Cauβπ·)) |
112 | 111 | expr 458 |
. . . . . . . . 9
β’ ((π β§ π β β) β
((β€β₯βπ) β dom πΉ β πΊ β (Cauβπ·))) |
113 | 52, 112 | biimtrrid 242 |
. . . . . . . 8
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ)π β dom πΉ β πΊ β (Cauβπ·))) |
114 | 113 | rexlimdva 3153 |
. . . . . . 7
β’ (π β (βπ β β βπ β (β€β₯βπ)π β dom πΉ β πΊ β (Cauβπ·))) |
115 | 51, 114 | mpd 15 |
. . . . . 6
β’ (π β πΊ β (Cauβπ·)) |
116 | | eqid 2737 |
. . . . . . . 8
β’ ((π FilMap πΊ)β(β€β₯ β
β)) = ((π FilMap
πΊ)β(β€β₯ β
β)) |
117 | 10, 116 | caucfil 24663 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ 1 β β€ β§
πΊ:ββΆπ) β (πΊ β (Cauβπ·) β ((π FilMap πΊ)β(β€β₯ β
β)) β (CauFilβπ·))) |
118 | 5, 40, 31, 117 | syl3anc 1372 |
. . . . . 6
β’ (π β (πΊ β (Cauβπ·) β ((π FilMap πΊ)β(β€β₯ β
β)) β (CauFilβπ·))) |
119 | 115, 118 | mpbid 231 |
. . . . 5
β’ (π β ((π FilMap πΊ)β(β€β₯ β
β)) β (CauFilβπ·)) |
120 | 6 | cmetcvg 24665 |
. . . . 5
β’ ((π· β (CMetβπ) β§ ((π FilMap πΊ)β(β€β₯ β
β)) β (CauFilβπ·)) β (π½ fLim ((π FilMap πΊ)β(β€β₯ β
β))) β β
) |
121 | 1, 119, 120 | syl2anc 585 |
. . . 4
β’ (π β (π½ fLim ((π FilMap πΊ)β(β€β₯ β
β))) β β
) |
122 | 38, 121 | eqnetrd 3012 |
. . 3
β’ (π β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)
β β
) |
123 | | n0 4311 |
. . 3
β’ (((π½ fLimf
(βfilGen(β€β₯ β β)))βπΊ) β β
β
βπ¦ π¦ β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)) |
124 | 122, 123 | sylib 217 |
. 2
β’ (π β βπ¦ π¦ β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)) |
125 | 10, 34 | lmflf 23372 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ 1 β β€ β§
πΊ:ββΆπ) β (πΊ(βπ‘βπ½)π¦ β π¦ β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ))) |
126 | 8, 40, 31, 125 | syl3anc 1372 |
. . . 4
β’ (π β (πΊ(βπ‘βπ½)π¦ β π¦ β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ))) |
127 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β πΉ β (π βpm
β)) |
128 | | lmcl 22664 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΊ(βπ‘βπ½)π¦) β π¦ β π) |
129 | 8, 128 | sylan 581 |
. . . . . . 7
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β π¦ β π) |
130 | 6, 5, 10, 40 | lmmbr3 24640 |
. . . . . . . . . 10
β’ (π β (πΊ(βπ‘βπ½)π¦ β (πΊ β (π βpm β) β§ π¦ β π β§ βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)))) |
131 | 130 | biimpa 478 |
. . . . . . . . 9
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β (πΊ β (π βpm β) β§ π¦ β π β§ βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) |
132 | 131 | simp3d 1145 |
. . . . . . . 8
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) |
133 | | r19.26 3115 |
. . . . . . . . . . 11
β’
(βπ§ β
β+ (βπ β β βπ β (β€β₯βπ)π β dom πΉ β§ βπ β β βπ β (β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β (βπ§ β β+ βπ β β βπ β
(β€β₯βπ)π β dom πΉ β§ βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) |
134 | 10 | rexanuz2 15241 |
. . . . . . . . . . . . 13
β’
(βπ β
β βπ β
(β€β₯βπ)(π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β (βπ β β βπ β (β€β₯βπ)π β dom πΉ β§ βπ β β βπ β (β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) |
135 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β π β dom πΉ) |
136 | 99 | ad2ant2lr 747 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β (πΊβπ) = (πΉβπ)) |
137 | | simprr2 1223 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β (πΊβπ) β π) |
138 | 136, 137 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β (πΉβπ) β π) |
139 | 136 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β ((πΊβπ)π·π¦) = ((πΉβπ)π·π¦)) |
140 | | simprr3 1224 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β ((πΊβπ)π·π¦) < π§) |
141 | 139, 140 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β ((πΉβπ)π·π¦) < π§) |
142 | 135, 138,
141 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§))) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§)) |
143 | 142 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β ((π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
144 | 86, 143 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β β β§ π β (β€β₯βπ))) β ((π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
145 | 144 | anassrs 469 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (β€β₯βπ)) β ((π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β (π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
146 | 145 | ralimdva 3165 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (βπ β
(β€β₯βπ)(π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
147 | 146 | reximdva 3166 |
. . . . . . . . . . . . 13
β’ (π β (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
148 | 134, 147 | biimtrrid 242 |
. . . . . . . . . . . 12
β’ (π β ((βπ β β βπ β
(β€β₯βπ)π β dom πΉ β§ βπ β β βπ β (β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
149 | 148 | ralimdv 3167 |
. . . . . . . . . . 11
β’ (π β (βπ§ β β+
(βπ β β
βπ β
(β€β₯βπ)π β dom πΉ β§ βπ β β βπ β (β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
150 | 133, 149 | biimtrrid 242 |
. . . . . . . . . 10
β’ (π β ((βπ§ β β+
βπ β β
βπ β
(β€β₯βπ)π β dom πΉ β§ βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§)) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
151 | 48, 150 | mpand 694 |
. . . . . . . . 9
β’ (π β (βπ§ β β+
βπ β β
βπ β
(β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
152 | 151 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β (βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΊ β§ (πΊβπ) β π β§ ((πΊβπ)π·π¦) < π§) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§))) |
153 | 132, 152 | mpd 15 |
. . . . . . 7
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§)) |
154 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β π· β (βMetβπ)) |
155 | | 1zzd 12541 |
. . . . . . . 8
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β 1 β β€) |
156 | 6, 154, 10, 155 | lmmbr3 24640 |
. . . . . . 7
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β (πΉ(βπ‘βπ½)π¦ β (πΉ β (π βpm β) β§ π¦ β π β§ βπ§ β β+ βπ β β βπ β
(β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π¦) < π§)))) |
157 | 127, 129,
153, 156 | mpbir3and 1343 |
. . . . . 6
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β πΉ(βπ‘βπ½)π¦) |
158 | | lmrel 22597 |
. . . . . . 7
β’ Rel
(βπ‘βπ½) |
159 | 158 | releldmi 5908 |
. . . . . 6
β’ (πΉ(βπ‘βπ½)π¦ β πΉ β dom
(βπ‘βπ½)) |
160 | 157, 159 | syl 17 |
. . . . 5
β’ ((π β§ πΊ(βπ‘βπ½)π¦) β πΉ β dom
(βπ‘βπ½)) |
161 | 160 | ex 414 |
. . . 4
β’ (π β (πΊ(βπ‘βπ½)π¦ β πΉ β dom
(βπ‘βπ½))) |
162 | 126, 161 | sylbird 260 |
. . 3
β’ (π β (π¦ β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)
β πΉ β dom
(βπ‘βπ½))) |
163 | 162 | exlimdv 1937 |
. 2
β’ (π β (βπ¦ π¦ β ((π½ fLimf (βfilGen(β€β₯
β β)))βπΊ)
β πΉ β dom
(βπ‘βπ½))) |
164 | 124, 163 | mpd 15 |
1
β’ (π β πΉ β dom
(βπ‘βπ½)) |