Metamath Proof Explorer


Theorem cmetcaulem

Description: Lemma for cmetcau . (Contributed by Mario Carneiro, 14-Oct-2015)

Ref Expression
Hypotheses cmetcau.1 J = MetOpen D
cmetcau.3 φ D CMet X
cmetcau.4 φ P X
cmetcau.5 φ F Cau D
cmetcau.6 G = x if x dom F F x P
Assertion cmetcaulem φ F dom t J

Proof

Step Hyp Ref Expression
1 cmetcau.1 J = MetOpen D
2 cmetcau.3 φ D CMet X
3 cmetcau.4 φ P X
4 cmetcau.5 φ F Cau D
5 cmetcau.6 G = x if x dom F F x P
6 cmetmet D CMet X D Met X
7 2 6 syl φ D Met X
8 metxmet D Met X D ∞Met X
9 7 8 syl φ D ∞Met X
10 1 mopntopon D ∞Met X J TopOn X
11 9 10 syl φ J TopOn X
12 1z 1
13 nnuz = 1
14 13 uzfbas 1 fBas
15 12 14 mp1i φ fBas
16 fgcl fBas filGen Fil
17 15 16 syl φ filGen Fil
18 elfvdm D CMet X X dom CMet
19 2 18 syl φ X dom CMet
20 cnex V
21 20 a1i φ V
22 caufpm D ∞Met X F Cau D F X 𝑝𝑚
23 9 4 22 syl2anc φ F X 𝑝𝑚
24 elpm2g X dom CMet V F X 𝑝𝑚 F : dom F X dom F
25 24 simprbda X dom CMet V F X 𝑝𝑚 F : dom F X
26 19 21 23 25 syl21anc φ F : dom F X
27 26 adantr φ x F : dom F X
28 27 ffvelrnda φ x x dom F F x X
29 3 ad2antrr φ x ¬ x dom F P X
30 28 29 ifclda φ x if x dom F F x P X
31 30 5 fmptd φ G : X
32 flfval J TopOn X filGen Fil G : X J fLimf filGen G = J fLim X FilMap G filGen
33 11 17 31 32 syl3anc φ J fLimf filGen G = J fLim X FilMap G filGen
34 eqid filGen = filGen
35 34 fmfg X dom CMet fBas G : X X FilMap G = X FilMap G filGen
36 19 15 31 35 syl3anc φ X FilMap G = X FilMap G filGen
37 36 oveq2d φ J fLim X FilMap G = J fLim X FilMap G filGen
38 33 37 eqtr4d φ J fLimf filGen G = J fLim X FilMap G
39 biidd z = 1 j k j k dom F j k j k dom F
40 1zzd φ 1
41 13 9 40 iscau3 φ F Cau D F X 𝑝𝑚 z + j k j k dom F F k X w k F k D F w < z
42 41 simplbda φ F Cau D z + j k j k dom F F k X w k F k D F w < z
43 4 42 mpdan φ z + j k j k dom F F k X w k F k D F w < z
44 simp1 k dom F F k X w k F k D F w < z k dom F
45 44 ralimi k j k dom F F k X w k F k D F w < z k j k dom F
46 45 reximi j k j k dom F F k X w k F k D F w < z j k j k dom F
47 46 ralimi z + j k j k dom F F k X w k F k D F w < z z + j k j k dom F
48 43 47 syl φ z + j k j k dom F
49 1rp 1 +
50 49 a1i φ 1 +
51 39 48 50 rspcdva φ j k j k dom F
52 dfss3 j dom F k j k dom F
53 nnsscn
54 31 53 jctir φ G : X
55 elpm2r X dom CMet V G : X G X 𝑝𝑚
56 19 21 54 55 syl21anc φ G X 𝑝𝑚
57 56 adantr φ j j dom F G X 𝑝𝑚
58 eqid j = j
59 9 adantr φ j j dom F D ∞Met X
60 nnz j j
61 60 ad2antrl φ j j dom F j
62 eqidd φ j j dom F k j F k = F k
63 eqidd φ j j dom F m j F m = F m
64 58 59 61 62 63 iscau4 φ j j dom F F Cau D F X 𝑝𝑚 z + m j k m k dom F F k X F k D F m < z
65 64 simplbda φ j j dom F F Cau D z + m j k m k dom F F k X F k D F m < z
66 4 65 mpidan φ j j dom F z + m j k m k dom F F k X F k D F m < z
67 simprl φ j j dom F j
68 eluznn j m j m
69 67 68 sylan φ j j dom F m j m
70 eluznn m k m k
71 5 30 dmmptd φ dom G =
72 71 adantr φ j j dom F dom G =
73 72 eleq2d φ j j dom F k dom G k
74 73 biimpar φ j j dom F k k dom G
75 74 a1d φ j j dom F k k dom F k dom G
76 idd φ j j dom F k F k X F k X
77 idd φ j j dom F k F k D F m < z F k D F m < z
78 75 76 77 3anim123d φ j j dom F k k dom F F k X F k D F m < z k dom G F k X F k D F m < z
79 70 78 sylan2 φ j j dom F m k m k dom F F k X F k D F m < z k dom G F k X F k D F m < z
80 79 anassrs φ j j dom F m k m k dom F F k X F k D F m < z k dom G F k X F k D F m < z
81 80 ralimdva φ j j dom F m k m k dom F F k X F k D F m < z k m k dom G F k X F k D F m < z
82 69 81 syldan φ j j dom F m j k m k dom F F k X F k D F m < z k m k dom G F k X F k D F m < z
83 82 reximdva φ j j dom F m j k m k dom F F k X F k D F m < z m j k m k dom G F k X F k D F m < z
84 83 ralimdv φ j j dom F z + m j k m k dom F F k X F k D F m < z z + m j k m k dom G F k X F k D F m < z
85 66 84 mpd φ j j dom F z + m j k m k dom G F k X F k D F m < z
86 eluznn j k j k
87 67 86 sylan φ j j dom F k j k
88 simprr φ j j dom F j dom F
89 88 sselda φ j j dom F k j k dom F
90 iftrue k dom F if k dom F F k P = F k
91 90 adantl k k dom F if k dom F F k P = F k
92 fvex F k V
93 91 92 eqeltrdi k k dom F if k dom F F k P V
94 eleq1w x = k x dom F k dom F
95 fveq2 x = k F x = F k
96 94 95 ifbieq1d x = k if x dom F F x P = if k dom F F k P
97 96 5 fvmptg k if k dom F F k P V G k = if k dom F F k P
98 93 97 syldan k k dom F G k = if k dom F F k P
99 98 91 eqtrd k k dom F G k = F k
100 87 89 99 syl2anc φ j j dom F k j G k = F k
101 88 sselda φ j j dom F m j m dom F
102 69 101 elind φ j j dom F m j m dom F
103 fveq2 k = m G k = G m
104 fveq2 k = m F k = F m
105 103 104 eqeq12d k = m G k = F k G m = F m
106 elin k dom F k k dom F
107 106 99 sylbi k dom F G k = F k
108 105 107 vtoclga m dom F G m = F m
109 102 108 syl φ j j dom F m j G m = F m
110 58 59 61 100 109 iscau4 φ j j dom F G Cau D G X 𝑝𝑚 z + m j k m k dom G F k X F k D F m < z
111 57 85 110 mpbir2and φ j j dom F G Cau D
112 111 expr φ j j dom F G Cau D
113 52 112 syl5bir φ j k j k dom F G Cau D
114 113 rexlimdva φ j k j k dom F G Cau D
115 51 114 mpd φ G Cau D
116 eqid X FilMap G = X FilMap G
117 13 116 caucfil D ∞Met X 1 G : X G Cau D X FilMap G CauFil D
118 9 40 31 117 syl3anc φ G Cau D X FilMap G CauFil D
119 115 118 mpbid φ X FilMap G CauFil D
120 1 cmetcvg D CMet X X FilMap G CauFil D J fLim X FilMap G
121 2 119 120 syl2anc φ J fLim X FilMap G
122 38 121 eqnetrd φ J fLimf filGen G
123 n0 J fLimf filGen G y y J fLimf filGen G
124 122 123 sylib φ y y J fLimf filGen G
125 13 34 lmflf J TopOn X 1 G : X G t J y y J fLimf filGen G
126 11 40 31 125 syl3anc φ G t J y y J fLimf filGen G
127 23 adantr φ G t J y F X 𝑝𝑚
128 lmcl J TopOn X G t J y y X
129 11 128 sylan φ G t J y y X
130 1 9 13 40 lmmbr3 φ G t J y G X 𝑝𝑚 y X z + j k j k dom G G k X G k D y < z
131 130 biimpa φ G t J y G X 𝑝𝑚 y X z + j k j k dom G G k X G k D y < z
132 131 simp3d φ G t J y z + j k j k dom G G k X G k D y < z
133 r19.26 z + j k j k dom F j k j k dom G G k X G k D y < z z + j k j k dom F z + j k j k dom G G k X G k D y < z
134 13 rexanuz2 j k j k dom F k dom G G k X G k D y < z j k j k dom F j k j k dom G G k X G k D y < z
135 simprl φ k k dom F k dom G G k X G k D y < z k dom F
136 99 ad2ant2lr φ k k dom F k dom G G k X G k D y < z G k = F k
137 simprr2 φ k k dom F k dom G G k X G k D y < z G k X
138 136 137 eqeltrrd φ k k dom F k dom G G k X G k D y < z F k X
139 136 oveq1d φ k k dom F k dom G G k X G k D y < z G k D y = F k D y
140 simprr3 φ k k dom F k dom G G k X G k D y < z G k D y < z
141 139 140 eqbrtrrd φ k k dom F k dom G G k X G k D y < z F k D y < z
142 135 138 141 3jca φ k k dom F k dom G G k X G k D y < z k dom F F k X F k D y < z
143 142 ex φ k k dom F k dom G G k X G k D y < z k dom F F k X F k D y < z
144 86 143 sylan2 φ j k j k dom F k dom G G k X G k D y < z k dom F F k X F k D y < z
145 144 anassrs φ j k j k dom F k dom G G k X G k D y < z k dom F F k X F k D y < z
146 145 ralimdva φ j k j k dom F k dom G G k X G k D y < z k j k dom F F k X F k D y < z
147 146 reximdva φ j k j k dom F k dom G G k X G k D y < z j k j k dom F F k X F k D y < z
148 134 147 syl5bir φ j k j k dom F j k j k dom G G k X G k D y < z j k j k dom F F k X F k D y < z
149 148 ralimdv φ z + j k j k dom F j k j k dom G G k X G k D y < z z + j k j k dom F F k X F k D y < z
150 133 149 syl5bir φ z + j k j k dom F z + j k j k dom G G k X G k D y < z z + j k j k dom F F k X F k D y < z
151 48 150 mpand φ z + j k j k dom G G k X G k D y < z z + j k j k dom F F k X F k D y < z
152 151 adantr φ G t J y z + j k j k dom G G k X G k D y < z z + j k j k dom F F k X F k D y < z
153 132 152 mpd φ G t J y z + j k j k dom F F k X F k D y < z
154 9 adantr φ G t J y D ∞Met X
155 1zzd φ G t J y 1
156 1 154 13 155 lmmbr3 φ G t J y F t J y F X 𝑝𝑚 y X z + j k j k dom F F k X F k D y < z
157 127 129 153 156 mpbir3and φ G t J y F t J y
158 lmrel Rel t J
159 158 releldmi F t J y F dom t J
160 157 159 syl φ G t J y F dom t J
161 160 ex φ G t J y F dom t J
162 126 161 sylbird φ y J fLimf filGen G F dom t J
163 162 exlimdv φ y y J fLimf filGen G F dom t J
164 124 163 mpd φ F dom t J