Metamath Proof Explorer


Theorem dvcnvlem

Description: Lemma for dvcnvre . (Contributed by Mario Carneiro, 25-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses dvcnv.j J = TopOpen fld
dvcnv.k K = J 𝑡 S
dvcnv.s φ S
dvcnv.y φ Y K
dvcnv.f φ F : X 1-1 onto Y
dvcnv.i φ F -1 : Y cn X
dvcnv.d φ dom F S = X
dvcnv.z φ ¬ 0 ran F S
dvcnv.c φ C X
Assertion dvcnvlem φ F C F -1 S 1 F S C

Proof

Step Hyp Ref Expression
1 dvcnv.j J = TopOpen fld
2 dvcnv.k K = J 𝑡 S
3 dvcnv.s φ S
4 dvcnv.y φ Y K
5 dvcnv.f φ F : X 1-1 onto Y
6 dvcnv.i φ F -1 : Y cn X
7 dvcnv.d φ dom F S = X
8 dvcnv.z φ ¬ 0 ran F S
9 dvcnv.c φ C X
10 f1of F : X 1-1 onto Y F : X Y
11 5 10 syl φ F : X Y
12 11 9 ffvelrnd φ F C Y
13 1 cnfldtopon J TopOn
14 recnprss S S
15 3 14 syl φ S
16 resttopon J TopOn S J 𝑡 S TopOn S
17 13 15 16 sylancr φ J 𝑡 S TopOn S
18 2 17 eqeltrid φ K TopOn S
19 topontop K TopOn S K Top
20 18 19 syl φ K Top
21 isopn3i K Top Y K int K Y = Y
22 20 4 21 syl2anc φ int K Y = Y
23 12 22 eleqtrrd φ F C int K Y
24 f1ocnv F : X 1-1 onto Y F -1 : Y 1-1 onto X
25 f1of F -1 : Y 1-1 onto X F -1 : Y X
26 5 24 25 3syl φ F -1 : Y X
27 eldifi z Y F C z Y
28 ffvelrn F -1 : Y X z Y F -1 z X
29 26 27 28 syl2an φ z Y F C F -1 z X
30 29 anim1i φ z Y F C F -1 z C F -1 z X F -1 z C
31 eldifsn F -1 z X C F -1 z X F -1 z C
32 30 31 sylibr φ z Y F C F -1 z C F -1 z X C
33 32 anasss φ z Y F C F -1 z C F -1 z X C
34 eldifi y X C y X
35 dvbsss dom F S S
36 7 35 eqsstrrdi φ X S
37 36 15 sstrd φ X
38 37 sselda φ y X y
39 34 38 sylan2 φ y X C y
40 36 9 sseldd φ C S
41 15 40 sseldd φ C
42 41 adantr φ y X C C
43 39 42 subcld φ y X C y C
44 toponss K TopOn S Y K Y S
45 18 4 44 syl2anc φ Y S
46 45 15 sstrd φ Y
47 11 46 fssd φ F : X
48 ffvelrn F : X y X F y
49 47 34 48 syl2an φ y X C F y
50 46 12 sseldd φ F C
51 50 adantr φ y X C F C
52 49 51 subcld φ y X C F y F C
53 eldifsni y X C y C
54 53 adantl φ y X C y C
55 49 51 subeq0ad φ y X C F y F C = 0 F y = F C
56 f1of1 F : X 1-1 onto Y F : X 1-1 Y
57 5 56 syl φ F : X 1-1 Y
58 57 adantr φ y X C F : X 1-1 Y
59 34 adantl φ y X C y X
60 9 adantr φ y X C C X
61 f1fveq F : X 1-1 Y y X C X F y = F C y = C
62 58 59 60 61 syl12anc φ y X C F y = F C y = C
63 55 62 bitrd φ y X C F y F C = 0 y = C
64 63 necon3bid φ y X C F y F C 0 y C
65 54 64 mpbird φ y X C F y F C 0
66 43 52 65 divcld φ y X C y C F y F C
67 limcresi F -1 lim F C F -1 Y F C lim F C
68 26 feqmptd φ F -1 = z Y F -1 z
69 68 reseq1d φ F -1 Y F C = z Y F -1 z Y F C
70 difss Y F C Y
71 resmpt Y F C Y z Y F -1 z Y F C = z Y F C F -1 z
72 70 71 ax-mp z Y F -1 z Y F C = z Y F C F -1 z
73 69 72 eqtrdi φ F -1 Y F C = z Y F C F -1 z
74 73 oveq1d φ F -1 Y F C lim F C = z Y F C F -1 z lim F C
75 67 74 sseqtrid φ F -1 lim F C z Y F C F -1 z lim F C
76 f1ocnvfv1 F : X 1-1 onto Y C X F -1 F C = C
77 5 9 76 syl2anc φ F -1 F C = C
78 6 12 cnlimci φ F -1 F C F -1 lim F C
79 77 78 eqeltrrd φ C F -1 lim F C
80 75 79 sseldd φ C z Y F C F -1 z lim F C
81 47 37 9 dvlem φ y X C F y F C y C
82 39 42 54 subne0d φ y X C y C 0
83 52 43 65 82 divne0d φ y X C F y F C y C 0
84 eldifsn F y F C y C 0 F y F C y C F y F C y C 0
85 81 83 84 sylanbrc φ y X C F y F C y C 0
86 85 fmpttd φ y X C F y F C y C : X C 0
87 difss 0
88 87 a1i φ 0
89 eqid J 𝑡 0 = J 𝑡 0
90 9 7 eleqtrrd φ C dom F S
91 dvfg S F S : dom F S
92 ffun F S : dom F S Fun F S
93 funfvbrb Fun F S C dom F S C F S F S C
94 3 91 92 93 4syl φ C dom F S C F S F S C
95 90 94 mpbid φ C F S F S C
96 eqid y X C F y F C y C = y X C F y F C y C
97 2 1 96 15 47 36 eldv φ C F S F S C C int K X F S C y X C F y F C y C lim C
98 95 97 mpbid φ C int K X F S C y X C F y F C y C lim C
99 98 simprd φ F S C y X C F y F C y C lim C
100 resttopon J TopOn 0 J 𝑡 0 TopOn 0
101 13 87 100 mp2an J 𝑡 0 TopOn 0
102 101 a1i φ J 𝑡 0 TopOn 0
103 13 a1i φ J TopOn
104 1cnd φ 1
105 102 103 104 cnmptc φ x 0 1 J 𝑡 0 Cn J
106 102 cnmptid φ x 0 x J 𝑡 0 Cn J 𝑡 0
107 1 89 divcn ÷ J × t J 𝑡 0 Cn J
108 107 a1i φ ÷ J × t J 𝑡 0 Cn J
109 102 105 106 108 cnmpt12f φ x 0 1 x J 𝑡 0 Cn J
110 3 91 syl φ F S : dom F S
111 7 feq2d φ F S : dom F S F S : X
112 110 111 mpbid φ F S : X
113 112 9 ffvelrnd φ F S C
114 110 ffnd φ F S Fn dom F S
115 fnfvelrn F S Fn dom F S C dom F S F S C ran F S
116 114 90 115 syl2anc φ F S C ran F S
117 nelne2 F S C ran F S ¬ 0 ran F S F S C 0
118 116 8 117 syl2anc φ F S C 0
119 eldifsn F S C 0 F S C F S C 0
120 113 118 119 sylanbrc φ F S C 0
121 101 toponunii 0 = J 𝑡 0
122 121 cncnpi x 0 1 x J 𝑡 0 Cn J F S C 0 x 0 1 x J 𝑡 0 CnP J F S C
123 109 120 122 syl2anc φ x 0 1 x J 𝑡 0 CnP J F S C
124 86 88 1 89 99 123 limccnp φ x 0 1 x F S C x 0 1 x y X C F y F C y C lim C
125 oveq2 x = F S C 1 x = 1 F S C
126 eqid x 0 1 x = x 0 1 x
127 ovex 1 F S C V
128 125 126 127 fvmpt F S C 0 x 0 1 x F S C = 1 F S C
129 120 128 syl φ x 0 1 x F S C = 1 F S C
130 eqidd φ y X C F y F C y C = y X C F y F C y C
131 eqidd φ x 0 1 x = x 0 1 x
132 oveq2 x = F y F C y C 1 x = 1 F y F C y C
133 85 130 131 132 fmptco φ x 0 1 x y X C F y F C y C = y X C 1 F y F C y C
134 52 43 65 82 recdivd φ y X C 1 F y F C y C = y C F y F C
135 134 mpteq2dva φ y X C 1 F y F C y C = y X C y C F y F C
136 133 135 eqtrd φ x 0 1 x y X C F y F C y C = y X C y C F y F C
137 136 oveq1d φ x 0 1 x y X C F y F C y C lim C = y X C y C F y F C lim C
138 124 129 137 3eltr3d φ 1 F S C y X C y C F y F C lim C
139 oveq1 y = F -1 z y C = F -1 z C
140 fveq2 y = F -1 z F y = F F -1 z
141 140 oveq1d y = F -1 z F y F C = F F -1 z F C
142 139 141 oveq12d y = F -1 z y C F y F C = F -1 z C F F -1 z F C
143 eldifsni z Y F C z F C
144 143 adantl φ z Y F C z F C
145 144 necomd φ z Y F C F C z
146 f1ocnvfvb F : X 1-1 onto Y C X z Y F C = z F -1 z = C
147 5 9 27 146 syl2an3an φ z Y F C F C = z F -1 z = C
148 147 necon3abid φ z Y F C F C z ¬ F -1 z = C
149 145 148 mpbid φ z Y F C ¬ F -1 z = C
150 149 pm2.21d φ z Y F C F -1 z = C F -1 z C F F -1 z F C = 1 F S C
151 150 impr φ z Y F C F -1 z = C F -1 z C F F -1 z F C = 1 F S C
152 33 66 80 138 142 151 limcco φ 1 F S C z Y F C F -1 z C F F -1 z F C lim F C
153 77 eqcomd φ C = F -1 F C
154 153 adantr φ z Y F C C = F -1 F C
155 154 oveq2d φ z Y F C F -1 z C = F -1 z F -1 F C
156 f1ocnvfv2 F : X 1-1 onto Y z Y F F -1 z = z
157 5 27 156 syl2an φ z Y F C F F -1 z = z
158 157 oveq1d φ z Y F C F F -1 z F C = z F C
159 155 158 oveq12d φ z Y F C F -1 z C F F -1 z F C = F -1 z F -1 F C z F C
160 159 mpteq2dva φ z Y F C F -1 z C F F -1 z F C = z Y F C F -1 z F -1 F C z F C
161 160 oveq1d φ z Y F C F -1 z C F F -1 z F C lim F C = z Y F C F -1 z F -1 F C z F C lim F C
162 152 161 eleqtrd φ 1 F S C z Y F C F -1 z F -1 F C z F C lim F C
163 eqid z Y F C F -1 z F -1 F C z F C = z Y F C F -1 z F -1 F C z F C
164 26 37 fssd φ F -1 : Y
165 2 1 163 15 164 45 eldv φ F C F -1 S 1 F S C F C int K Y 1 F S C z Y F C F -1 z F -1 F C z F C lim F C
166 23 162 165 mpbir2and φ F C F -1 S 1 F S C