Metamath Proof Explorer


Theorem ptcnplem

Description: Lemma for ptcnp . (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses ptcnp.2 K = 𝑡 F
ptcnp.3 φ J TopOn X
ptcnp.4 φ I V
ptcnp.5 φ F : I Top
ptcnp.6 φ D X
ptcnp.7 φ k I x X A J CnP F k D
ptcnplem.1 k ψ
ptcnplem.2 φ ψ G Fn I
ptcnplem.3 φ ψ k I G k F k
ptcnplem.4 φ ψ W Fin
ptcnplem.5 φ ψ k I W G k = F k
ptcnplem.6 φ ψ x X k I A D k I G k
Assertion ptcnplem φ ψ z J D z x X k I A z k I G k

Proof

Step Hyp Ref Expression
1 ptcnp.2 K = 𝑡 F
2 ptcnp.3 φ J TopOn X
3 ptcnp.4 φ I V
4 ptcnp.5 φ F : I Top
5 ptcnp.6 φ D X
6 ptcnp.7 φ k I x X A J CnP F k D
7 ptcnplem.1 k ψ
8 ptcnplem.2 φ ψ G Fn I
9 ptcnplem.3 φ ψ k I G k F k
10 ptcnplem.4 φ ψ W Fin
11 ptcnplem.5 φ ψ k I W G k = F k
12 ptcnplem.6 φ ψ x X k I A D k I G k
13 inss2 I W W
14 ssfi W Fin I W W I W Fin
15 10 13 14 sylancl φ ψ I W Fin
16 nfv k φ
17 16 7 nfan k φ ψ
18 elinel1 k I W k I
19 6 adantlr φ ψ k I x X A J CnP F k D
20 5 adantr φ ψ D X
21 simpr φ k I x X x X
22 2 adantr φ k I J TopOn X
23 4 ffvelrnda φ k I F k Top
24 toptopon2 F k Top F k TopOn F k
25 23 24 sylib φ k I F k TopOn F k
26 cnpf2 J TopOn X F k TopOn F k x X A J CnP F k D x X A : X F k
27 22 25 6 26 syl3anc φ k I x X A : X F k
28 eqid x X A = x X A
29 28 fmpt x X A F k x X A : X F k
30 27 29 sylibr φ k I x X A F k
31 30 r19.21bi φ k I x X A F k
32 28 fvmpt2 x X A F k x X A x = A
33 21 31 32 syl2anc φ k I x X x X A x = A
34 33 an32s φ x X k I x X A x = A
35 34 mpteq2dva φ x X k I x X A x = k I A
36 simpr φ x X x X
37 3 adantr φ x X I V
38 37 mptexd φ x X k I A V
39 eqid x X k I A = x X k I A
40 39 fvmpt2 x X k I A V x X k I A x = k I A
41 36 38 40 syl2anc φ x X x X k I A x = k I A
42 35 41 eqtr4d φ x X k I x X A x = x X k I A x
43 42 ralrimiva φ x X k I x X A x = x X k I A x
44 43 adantr φ ψ x X k I x X A x = x X k I A x
45 nfcv _ x I
46 nffvmpt1 _ x x X A D
47 45 46 nfmpt _ x k I x X A D
48 nffvmpt1 _ x x X k I A D
49 47 48 nfeq x k I x X A D = x X k I A D
50 fveq2 x = D x X A x = x X A D
51 50 mpteq2dv x = D k I x X A x = k I x X A D
52 fveq2 x = D x X k I A x = x X k I A D
53 51 52 eqeq12d x = D k I x X A x = x X k I A x k I x X A D = x X k I A D
54 49 53 rspc D X x X k I x X A x = x X k I A x k I x X A D = x X k I A D
55 20 44 54 sylc φ ψ k I x X A D = x X k I A D
56 55 12 eqeltrd φ ψ k I x X A D k I G k
57 3 adantr φ ψ I V
58 mptelixpg I V k I x X A D k I G k k I x X A D G k
59 57 58 syl φ ψ k I x X A D k I G k k I x X A D G k
60 56 59 mpbid φ ψ k I x X A D G k
61 60 r19.21bi φ ψ k I x X A D G k
62 cnpimaex x X A J CnP F k D G k F k x X A D G k u J D u x X A u G k
63 19 9 61 62 syl3anc φ ψ k I u J D u x X A u G k
64 18 63 sylan2 φ ψ k I W u J D u x X A u G k
65 64 ex φ ψ k I W u J D u x X A u G k
66 17 65 ralrimi φ ψ k I W u J D u x X A u G k
67 eleq2 u = f k D u D f k
68 imaeq2 u = f k x X A u = x X A f k
69 68 sseq1d u = f k x X A u G k x X A f k G k
70 67 69 anbi12d u = f k D u x X A u G k D f k x X A f k G k
71 70 ac6sfi I W Fin k I W u J D u x X A u G k f f : I W J k I W D f k x X A f k G k
72 15 66 71 syl2anc φ ψ f f : I W J k I W D f k x X A f k G k
73 2 ad2antrr φ ψ f : I W J k I W D f k x X A f k G k J TopOn X
74 toponuni J TopOn X X = J
75 73 74 syl φ ψ f : I W J k I W D f k x X A f k G k X = J
76 75 ineq1d φ ψ f : I W J k I W D f k x X A f k G k X ran f = J ran f
77 topontop J TopOn X J Top
78 2 77 syl φ J Top
79 78 ad2antrr φ ψ f : I W J k I W D f k x X A f k G k J Top
80 frn f : I W J ran f J
81 80 ad2antrl φ ψ f : I W J k I W D f k x X A f k G k ran f J
82 15 adantr φ ψ f : I W J k I W D f k x X A f k G k I W Fin
83 ffn f : I W J f Fn I W
84 83 ad2antrl φ ψ f : I W J k I W D f k x X A f k G k f Fn I W
85 dffn4 f Fn I W f : I W onto ran f
86 84 85 sylib φ ψ f : I W J k I W D f k x X A f k G k f : I W onto ran f
87 fofi I W Fin f : I W onto ran f ran f Fin
88 82 86 87 syl2anc φ ψ f : I W J k I W D f k x X A f k G k ran f Fin
89 eqid J = J
90 89 rintopn J Top ran f J ran f Fin J ran f J
91 79 81 88 90 syl3anc φ ψ f : I W J k I W D f k x X A f k G k J ran f J
92 76 91 eqeltrd φ ψ f : I W J k I W D f k x X A f k G k X ran f J
93 5 ad2antrr φ ψ f : I W J k I W D f k x X A f k G k D X
94 simpl D f k x X A f k G k D f k
95 94 ralimi k I W D f k x X A f k G k k I W D f k
96 95 ad2antll φ ψ f : I W J k I W D f k x X A f k G k k I W D f k
97 eleq2 z = f k D z D f k
98 97 ralrn f Fn I W z ran f D z k I W D f k
99 84 98 syl φ ψ f : I W J k I W D f k x X A f k G k z ran f D z k I W D f k
100 96 99 mpbird φ ψ f : I W J k I W D f k x X A f k G k z ran f D z
101 elrint D X ran f D X z ran f D z
102 93 100 101 sylanbrc φ ψ f : I W J k I W D f k x X A f k G k D X ran f
103 nfv k f : I W J
104 17 103 nfan k φ ψ f : I W J
105 funmpt Fun x X A
106 simp-4l φ ψ f : I W J k I W D f k φ
107 106 2 syl φ ψ f : I W J k I W D f k J TopOn X
108 simpllr φ ψ f : I W J k I W D f k f : I W J
109 simplr φ ψ f : I W J k I W D f k k I W
110 108 109 ffvelrnd φ ψ f : I W J k I W D f k f k J
111 toponss J TopOn X f k J f k X
112 107 110 111 syl2anc φ ψ f : I W J k I W D f k f k X
113 109 elin1d φ ψ f : I W J k I W D f k k I
114 106 113 30 syl2anc φ ψ f : I W J k I W D f k x X A F k
115 dmmptg x X A F k dom x X A = X
116 114 115 syl φ ψ f : I W J k I W D f k dom x X A = X
117 112 116 sseqtrrd φ ψ f : I W J k I W D f k f k dom x X A
118 funimass4 Fun x X A f k dom x X A x X A f k G k t f k x X A t G k
119 105 117 118 sylancr φ ψ f : I W J k I W D f k x X A f k G k t f k x X A t G k
120 nffvmpt1 _ x x X A t
121 120 nfel1 x x X A t G k
122 nfv t x X A x G k
123 fveq2 t = x x X A t = x X A x
124 123 eleq1d t = x x X A t G k x X A x G k
125 121 122 124 cbvralw t f k x X A t G k x f k x X A x G k
126 119 125 bitrdi φ ψ f : I W J k I W D f k x X A f k G k x f k x X A x G k
127 inss1 X ran f X
128 ssralv X ran f X x X A F k x X ran f A F k
129 127 114 128 mpsyl φ ψ f : I W J k I W D f k x X ran f A F k
130 inss2 X ran f ran f
131 108 83 syl φ ψ f : I W J k I W D f k f Fn I W
132 fnfvelrn f Fn I W k I W f k ran f
133 131 109 132 syl2anc φ ψ f : I W J k I W D f k f k ran f
134 intss1 f k ran f ran f f k
135 133 134 syl φ ψ f : I W J k I W D f k ran f f k
136 130 135 sstrid φ ψ f : I W J k I W D f k X ran f f k
137 ssralv X ran f f k x f k x X A x G k x X ran f x X A x G k
138 136 137 syl φ ψ f : I W J k I W D f k x f k x X A x G k x X ran f x X A x G k
139 r19.26 x X ran f A F k x X A x G k x X ran f A F k x X ran f x X A x G k
140 elinel1 x X ran f x X
141 140 32 sylan x X ran f A F k x X A x = A
142 141 eleq1d x X ran f A F k x X A x G k A G k
143 142 biimpd x X ran f A F k x X A x G k A G k
144 143 expimpd x X ran f A F k x X A x G k A G k
145 144 ralimia x X ran f A F k x X A x G k x X ran f A G k
146 139 145 sylbir x X ran f A F k x X ran f x X A x G k x X ran f A G k
147 129 138 146 syl6an φ ψ f : I W J k I W D f k x f k x X A x G k x X ran f A G k
148 126 147 sylbid φ ψ f : I W J k I W D f k x X A f k G k x X ran f A G k
149 148 expimpd φ ψ f : I W J k I W D f k x X A f k G k x X ran f A G k
150 104 149 ralimdaa φ ψ f : I W J k I W D f k x X A f k G k k I W x X ran f A G k
151 150 impr φ ψ f : I W J k I W D f k x X A f k G k k I W x X ran f A G k
152 simpl φ ψ φ
153 eldifi k I W k I
154 140 31 sylan2 φ k I x X ran f A F k
155 154 ralrimiva φ k I x X ran f A F k
156 152 153 155 syl2an φ ψ k I W x X ran f A F k
157 eleq2 G k = F k A G k A F k
158 157 ralbidv G k = F k x X ran f A G k x X ran f A F k
159 11 158 syl φ ψ k I W x X ran f A G k x X ran f A F k
160 156 159 mpbird φ ψ k I W x X ran f A G k
161 160 ex φ ψ k I W x X ran f A G k
162 17 161 ralrimi φ ψ k I W x X ran f A G k
163 162 adantr φ ψ f : I W J k I W D f k x X A f k G k k I W x X ran f A G k
164 inundif I W I W = I
165 164 raleqi k I W I W x X ran f A G k k I x X ran f A G k
166 ralunb k I W I W x X ran f A G k k I W x X ran f A G k k I W x X ran f A G k
167 165 166 bitr3i k I x X ran f A G k k I W x X ran f A G k k I W x X ran f A G k
168 151 163 167 sylanbrc φ ψ f : I W J k I W D f k x X A f k G k k I x X ran f A G k
169 ralcom x X ran f k I A G k k I x X ran f A G k
170 168 169 sylibr φ ψ f : I W J k I W D f k x X A f k G k x X ran f k I A G k
171 3 ad2antrr φ ψ f : I W J k I W D f k x X A f k G k I V
172 nffvmpt1 _ x x X k I A t
173 172 nfel1 x x X k I A t k I G k
174 nfv t x X k I A x k I G k
175 fveq2 t = x x X k I A t = x X k I A x
176 175 eleq1d t = x x X k I A t k I G k x X k I A x k I G k
177 173 174 176 cbvralw t X ran f x X k I A t k I G k x X ran f x X k I A x k I G k
178 mptexg I V k I A V
179 140 178 40 syl2anr I V x X ran f x X k I A x = k I A
180 179 eleq1d I V x X ran f x X k I A x k I G k k I A k I G k
181 mptelixpg I V k I A k I G k k I A G k
182 181 adantr I V x X ran f k I A k I G k k I A G k
183 180 182 bitrd I V x X ran f x X k I A x k I G k k I A G k
184 183 ralbidva I V x X ran f x X k I A x k I G k x X ran f k I A G k
185 177 184 syl5bb I V t X ran f x X k I A t k I G k x X ran f k I A G k
186 171 185 syl φ ψ f : I W J k I W D f k x X A f k G k t X ran f x X k I A t k I G k x X ran f k I A G k
187 170 186 mpbird φ ψ f : I W J k I W D f k x X A f k G k t X ran f x X k I A t k I G k
188 funmpt Fun x X k I A
189 3 mptexd φ k I A V
190 189 ralrimivw φ x X k I A V
191 190 ad2antrr φ ψ f : I W J k I W D f k x X A f k G k x X k I A V
192 dmmptg x X k I A V dom x X k I A = X
193 191 192 syl φ ψ f : I W J k I W D f k x X A f k G k dom x X k I A = X
194 127 193 sseqtrrid φ ψ f : I W J k I W D f k x X A f k G k X ran f dom x X k I A
195 funimass4 Fun x X k I A X ran f dom x X k I A x X k I A X ran f k I G k t X ran f x X k I A t k I G k
196 188 194 195 sylancr φ ψ f : I W J k I W D f k x X A f k G k x X k I A X ran f k I G k t X ran f x X k I A t k I G k
197 187 196 mpbird φ ψ f : I W J k I W D f k x X A f k G k x X k I A X ran f k I G k
198 eleq2 z = X ran f D z D X ran f
199 imaeq2 z = X ran f x X k I A z = x X k I A X ran f
200 199 sseq1d z = X ran f x X k I A z k I G k x X k I A X ran f k I G k
201 198 200 anbi12d z = X ran f D z x X k I A z k I G k D X ran f x X k I A X ran f k I G k
202 201 rspcev X ran f J D X ran f x X k I A X ran f k I G k z J D z x X k I A z k I G k
203 92 102 197 202 syl12anc φ ψ f : I W J k I W D f k x X A f k G k z J D z x X k I A z k I G k
204 72 203 exlimddv φ ψ z J D z x X k I A z k I G k