Step | Hyp | Ref
| Expression |
1 | | cmetmet 23084 |
. . . . . . . . 9
|
2 | | metxmet 22139 |
. . . . . . . . 9
|
3 | 1, 2 | syl 17 |
. . . . . . . 8
|
4 | 3 | adantr 481 |
. . . . . . 7
|
5 | | cmetss.2 |
. . . . . . . 8
|
6 | 5 | mopntopon 22244 |
. . . . . . 7
TopOn |
7 | 4, 6 | syl 17 |
. . . . . 6
TopOn |
8 | | resss 5422 |
. . . . . . . 8
|
9 | | dmss 5323 |
. . . . . . . 8
|
10 | | dmss 5323 |
. . . . . . . 8
|
11 | 8, 9, 10 | mp2b 10 |
. . . . . . 7
|
12 | | cmetmet 23084 |
. . . . . . . . 9
|
13 | | metdmdm 22141 |
. . . . . . . . 9
|
14 | 12, 13 | syl 17 |
. . . . . . . 8
|
15 | | metdmdm 22141 |
. . . . . . . . 9
|
16 | 1, 15 | syl 17 |
. . . . . . . 8
|
17 | | sseq12 3628 |
. . . . . . . 8
|
18 | 14, 16, 17 | syl2anr 495 |
. . . . . . 7
|
19 | 11, 18 | mpbiri 248 |
. . . . . 6
|
20 | | flimcls 21789 |
. . . . . 6
TopOn
|
21 | 7, 19, 20 | syl2anc 693 |
. . . . 5
|
22 | | simprrr 805 |
. . . . . . 7
|
23 | 4 | adantr 481 |
. . . . . . . . 9
|
24 | 5 | methaus 22325 |
. . . . . . . . 9
|
25 | | hausflimi 21784 |
. . . . . . . . 9
|
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . 8
|
27 | 23, 6 | syl 17 |
. . . . . . . . . . . 12
TopOn |
28 | | simprl 794 |
. . . . . . . . . . . 12
|
29 | | simprrl 804 |
. . . . . . . . . . . 12
|
30 | | flimrest 21787 |
. . . . . . . . . . . 12
TopOn
↾t ↾t |
31 | 27, 28, 29, 30 | syl3anc 1326 |
. . . . . . . . . . 11
↾t ↾t |
32 | 19 | adantr 481 |
. . . . . . . . . . . . 13
|
33 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
34 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
35 | 33, 5, 34 | metrest 22329 |
. . . . . . . . . . . . 13
↾t
|
36 | 23, 32, 35 | syl2anc 693 |
. . . . . . . . . . . 12
↾t
|
37 | 36 | oveq1d 6665 |
. . . . . . . . . . 11
↾t ↾t ↾t |
38 | 31, 37 | eqtr3d 2658 |
. . . . . . . . . 10
↾t |
39 | | simplr 792 |
. . . . . . . . . . 11
|
40 | 5 | flimcfil 23112 |
. . . . . . . . . . . . 13
CauFil |
41 | 23, 22, 40 | syl2anc 693 |
. . . . . . . . . . . 12
CauFil |
42 | | cfilres 23094 |
. . . . . . . . . . . . 13
CauFil ↾t CauFil |
43 | 23, 28, 29, 42 | syl3anc 1326 |
. . . . . . . . . . . 12
CauFil ↾t CauFil |
44 | 41, 43 | mpbid 222 |
. . . . . . . . . . 11
↾t CauFil
|
45 | 34 | cmetcvg 23083 |
. . . . . . . . . . 11
↾t CauFil
↾t |
46 | 39, 44, 45 | syl2anc 693 |
. . . . . . . . . 10
↾t |
47 | 38, 46 | eqnetrd 2861 |
. . . . . . . . 9
|
48 | | n0 3931 |
. . . . . . . . . 10
|
49 | | elin 3796 |
. . . . . . . . . . 11
|
50 | 49 | exbii 1774 |
. . . . . . . . . 10
|
51 | 48, 50 | bitri 264 |
. . . . . . . . 9
|
52 | 47, 51 | sylib 208 |
. . . . . . . 8
|
53 | | mopick 2535 |
. . . . . . . 8
|
54 | 26, 52, 53 | syl2anc 693 |
. . . . . . 7
|
55 | 22, 54 | mpd 15 |
. . . . . 6
|
56 | 55 | rexlimdvaa 3032 |
. . . . 5
|
57 | 21, 56 | sylbid 230 |
. . . 4
|
58 | 57 | ssrdv 3609 |
. . 3
|
59 | 5 | mopntop 22245 |
. . . . 5
|
60 | 4, 59 | syl 17 |
. . . 4
|
61 | 5 | mopnuni 22246 |
. . . . . 6
|
62 | 4, 61 | syl 17 |
. . . . 5
|
63 | 19, 62 | sseqtrd 3641 |
. . . 4
|
64 | | eqid 2622 |
. . . . 5
|
65 | 64 | iscld4 20869 |
. . . 4
|
66 | 60, 63, 65 | syl2anc 693 |
. . 3
|
67 | 58, 66 | mpbird 247 |
. 2
|
68 | 1 | adantr 481 |
. . . 4
|
69 | 64 | cldss 20833 |
. . . . . 6
|
70 | 69 | adantl 482 |
. . . . 5
|
71 | 68, 2, 61 | 3syl 18 |
. . . . 5
|
72 | 70, 71 | sseqtr4d 3642 |
. . . 4
|
73 | | metres2 22168 |
. . . 4
|
74 | 68, 72, 73 | syl2anc 693 |
. . 3
|
75 | 3 | ad2antrr 762 |
. . . . . . . . 9
CauFil |
76 | 72 | adantr 481 |
. . . . . . . . 9
CauFil |
77 | 75, 76, 35 | syl2anc 693 |
. . . . . . . 8
CauFil ↾t
|
78 | 77 | eqcomd 2628 |
. . . . . . 7
CauFil
↾t |
79 | | metxmet 22139 |
. . . . . . . . . . 11
|
80 | 74, 79 | syl 17 |
. . . . . . . . . 10
|
81 | | cfilfil 23065 |
. . . . . . . . . 10
CauFil |
82 | 80, 81 | sylan 488 |
. . . . . . . . 9
CauFil |
83 | | elfvdm 6220 |
. . . . . . . . . 10
|
84 | 83 | ad2antrr 762 |
. . . . . . . . 9
CauFil |
85 | | trfg 21695 |
. . . . . . . . 9
↾t |
86 | 82, 76, 84, 85 | syl3anc 1326 |
. . . . . . . 8
CauFil ↾t |
87 | 86 | eqcomd 2628 |
. . . . . . 7
CauFil
↾t |
88 | 78, 87 | oveq12d 6668 |
. . . . . 6
CauFil ↾t ↾t |
89 | 75, 6 | syl 17 |
. . . . . . 7
CauFil TopOn |
90 | | filfbas 21652 |
. . . . . . . . . 10
|
91 | 82, 90 | syl 17 |
. . . . . . . . 9
CauFil |
92 | | filsspw 21655 |
. . . . . . . . . . 11
|
93 | 82, 92 | syl 17 |
. . . . . . . . . 10
CauFil |
94 | | sspwb 4917 |
. . . . . . . . . . 11
|
95 | 76, 94 | sylib 208 |
. . . . . . . . . 10
CauFil |
96 | 93, 95 | sstrd 3613 |
. . . . . . . . 9
CauFil |
97 | | fbasweak 21669 |
. . . . . . . . 9
|
98 | 91, 96, 84, 97 | syl3anc 1326 |
. . . . . . . 8
CauFil |
99 | | fgcl 21682 |
. . . . . . . 8
|
100 | 98, 99 | syl 17 |
. . . . . . 7
CauFil |
101 | | ssfg 21676 |
. . . . . . . . 9
|
102 | 98, 101 | syl 17 |
. . . . . . . 8
CauFil |
103 | | filtop 21659 |
. . . . . . . . 9
|
104 | 82, 103 | syl 17 |
. . . . . . . 8
CauFil |
105 | 102, 104 | sseldd 3604 |
. . . . . . 7
CauFil |
106 | | flimrest 21787 |
. . . . . . 7
TopOn
↾t
↾t
|
107 | 89, 100, 105, 106 | syl3anc 1326 |
. . . . . 6
CauFil
↾t ↾t |
108 | | flimclsi 21782 |
. . . . . . . . 9
|
109 | 105, 108 | syl 17 |
. . . . . . . 8
CauFil |
110 | | cldcls 20846 |
. . . . . . . . 9
|
111 | 110 | ad2antlr 763 |
. . . . . . . 8
CauFil |
112 | 109, 111 | sseqtrd 3641 |
. . . . . . 7
CauFil |
113 | | df-ss 3588 |
. . . . . . 7
|
114 | 112, 113 | sylib 208 |
. . . . . 6
CauFil |
115 | 88, 107, 114 | 3eqtrd 2660 |
. . . . 5
CauFil |
116 | | simpll 790 |
. . . . . 6
CauFil |
117 | 68, 2 | syl 17 |
. . . . . . 7
|
118 | | cfilresi 23093 |
. . . . . . 7
CauFil CauFil |
119 | 117, 118 | sylan 488 |
. . . . . 6
CauFil CauFil |
120 | 5 | cmetcvg 23083 |
. . . . . 6
CauFil
|
121 | 116, 119,
120 | syl2anc 693 |
. . . . 5
CauFil |
122 | 115, 121 | eqnetrd 2861 |
. . . 4
CauFil |
123 | 122 | ralrimiva 2966 |
. . 3
CauFil |
124 | 34 | iscmet 23082 |
. . 3
CauFil |
125 | 74, 123, 124 | sylanbrc 698 |
. 2
|
126 | 67, 125 | impbida 877 |
1
|