Metamath Proof Explorer


Theorem axdc4lem

Description: Lemma for axdc4 . (Contributed by Mario Carneiro, 31-Jan-2013) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Hypotheses axdc4lem.1 A V
axdc4lem.2 G = n ω , x A suc n × n F x
Assertion axdc4lem C A F : ω × A 𝒫 A g g : ω A g = C k ω g suc k k F g k

Proof

Step Hyp Ref Expression
1 axdc4lem.1 A V
2 axdc4lem.2 G = n ω , x A suc n × n F x
3 peano1 ω
4 opelxpi ω C A C ω × A
5 3 4 mpan C A C ω × A
6 simp2 F : ω × A 𝒫 A n ω x A n ω
7 fovrn F : ω × A 𝒫 A n ω x A n F x 𝒫 A
8 peano2 n ω suc n ω
9 8 snssd n ω suc n ω
10 eldifi n F x 𝒫 A n F x 𝒫 A
11 1 elpw2 n F x 𝒫 A n F x A
12 xpss12 suc n ω n F x A suc n × n F x ω × A
13 11 12 sylan2b suc n ω n F x 𝒫 A suc n × n F x ω × A
14 9 10 13 syl2an n ω n F x 𝒫 A suc n × n F x ω × A
15 snex suc n V
16 ovex n F x V
17 15 16 xpex suc n × n F x V
18 17 elpw suc n × n F x 𝒫 ω × A suc n × n F x ω × A
19 14 18 sylibr n ω n F x 𝒫 A suc n × n F x 𝒫 ω × A
20 6 7 19 syl2anc F : ω × A 𝒫 A n ω x A suc n × n F x 𝒫 ω × A
21 eldifn n F x 𝒫 A ¬ n F x
22 16 elsn n F x n F x =
23 22 necon3bbii ¬ n F x n F x
24 vex n V
25 24 sucex suc n V
26 25 snnz suc n
27 xpnz suc n n F x suc n × n F x
28 27 biimpi suc n n F x suc n × n F x
29 26 28 mpan n F x suc n × n F x
30 23 29 sylbi ¬ n F x suc n × n F x
31 17 elsn suc n × n F x suc n × n F x =
32 31 necon3bbii ¬ suc n × n F x suc n × n F x
33 30 32 sylibr ¬ n F x ¬ suc n × n F x
34 7 21 33 3syl F : ω × A 𝒫 A n ω x A ¬ suc n × n F x
35 20 34 eldifd F : ω × A 𝒫 A n ω x A suc n × n F x 𝒫 ω × A
36 35 3expib F : ω × A 𝒫 A n ω x A suc n × n F x 𝒫 ω × A
37 36 ralrimivv F : ω × A 𝒫 A n ω x A suc n × n F x 𝒫 ω × A
38 2 fmpo n ω x A suc n × n F x 𝒫 ω × A G : ω × A 𝒫 ω × A
39 37 38 sylib F : ω × A 𝒫 A G : ω × A 𝒫 ω × A
40 dcomex ω V
41 40 1 xpex ω × A V
42 41 axdc3 C ω × A G : ω × A 𝒫 ω × A h h : ω ω × A h = C k ω h suc k G h k
43 5 39 42 syl2an C A F : ω × A 𝒫 A h h : ω ω × A h = C k ω h suc k G h k
44 2ndcof h : ω ω × A 2 nd h : ω A
45 44 3ad2ant1 h : ω ω × A h = C k ω h suc k G h k 2 nd h : ω A
46 45 adantl C A h : ω ω × A h = C k ω h suc k G h k 2 nd h : ω A
47 fex2 2 nd h : ω A ω V A V 2 nd h V
48 40 1 47 mp3an23 2 nd h : ω A 2 nd h V
49 46 48 syl C A h : ω ω × A h = C k ω h suc k G h k 2 nd h V
50 fvco3 h : ω ω × A ω 2 nd h = 2 nd h
51 3 50 mpan2 h : ω ω × A 2 nd h = 2 nd h
52 51 3ad2ant1 h : ω ω × A h = C k ω h suc k G h k 2 nd h = 2 nd h
53 fveq2 h = C 2 nd h = 2 nd C
54 53 3ad2ant2 h : ω ω × A h = C k ω h suc k G h k 2 nd h = 2 nd C
55 52 54 eqtrd h : ω ω × A h = C k ω h suc k G h k 2 nd h = 2 nd C
56 op2ndg ω C A 2 nd C = C
57 3 56 mpan C A 2 nd C = C
58 55 57 sylan9eqr C A h : ω ω × A h = C k ω h suc k G h k 2 nd h = C
59 nfv k C A
60 nfv k h : ω ω × A
61 nfv k h = C
62 nfra1 k k ω h suc k G h k
63 60 61 62 nf3an k h : ω ω × A h = C k ω h suc k G h k
64 59 63 nfan k C A h : ω ω × A h = C k ω h suc k G h k
65 fveq2 m = h m = h
66 opeq1 m = m z = z
67 65 66 eqeq12d m = h m = m z h = z
68 67 exbidv m = z h m = m z z h = z
69 fveq2 m = i h m = h i
70 opeq1 m = i m z = i z
71 69 70 eqeq12d m = i h m = m z h i = i z
72 71 exbidv m = i z h m = m z z h i = i z
73 fveq2 m = suc i h m = h suc i
74 opeq1 m = suc i m z = suc i z
75 73 74 eqeq12d m = suc i h m = m z h suc i = suc i z
76 75 exbidv m = suc i z h m = m z z h suc i = suc i z
77 opeq2 z = C z = C
78 77 eqeq2d z = C h = z h = C
79 78 spcegv C A h = C z h = z
80 79 imp C A h = C z h = z
81 80 3ad2antr2 C A h : ω ω × A h = C k ω h suc k G h k z h = z
82 fveq2 h i = i z G h i = G i z
83 df-ov i G z = G i z
84 82 83 eqtr4di h i = i z G h i = i G z
85 84 adantl h : ω ω × A i ω h i = i z G h i = i G z
86 simplr h : ω ω × A i ω h i = i z i ω
87 ffvelrn h : ω ω × A i ω h i ω × A
88 eleq1 h i = i z h i ω × A i z ω × A
89 opelxp2 i z ω × A z A
90 88 89 syl6bi h i = i z h i ω × A z A
91 87 90 mpan9 h : ω ω × A i ω h i = i z z A
92 suceq n = i suc n = suc i
93 92 sneqd n = i suc n = suc i
94 oveq1 n = i n F x = i F x
95 93 94 xpeq12d n = i suc n × n F x = suc i × i F x
96 oveq2 x = z i F x = i F z
97 96 xpeq2d x = z suc i × i F x = suc i × i F z
98 snex suc i V
99 ovex i F z V
100 98 99 xpex suc i × i F z V
101 95 97 2 100 ovmpo i ω z A i G z = suc i × i F z
102 86 91 101 syl2anc h : ω ω × A i ω h i = i z i G z = suc i × i F z
103 85 102 eqtrd h : ω ω × A i ω h i = i z G h i = suc i × i F z
104 suceq k = i suc k = suc i
105 104 fveq2d k = i h suc k = h suc i
106 2fveq3 k = i G h k = G h i
107 105 106 eleq12d k = i h suc k G h k h suc i G h i
108 107 rspcv i ω k ω h suc k G h k h suc i G h i
109 108 ad2antlr h : ω ω × A i ω h i = i z k ω h suc k G h k h suc i G h i
110 eleq2 G h i = suc i × i F z h suc i G h i h suc i suc i × i F z
111 elxp h suc i suc i × i F z s t h suc i = s t s suc i t i F z
112 velsn s suc i s = suc i
113 opeq1 s = suc i s t = suc i t
114 112 113 sylbi s suc i s t = suc i t
115 114 eqeq2d s suc i h suc i = s t h suc i = suc i t
116 115 biimpac h suc i = s t s suc i h suc i = suc i t
117 116 adantrr h suc i = s t s suc i t i F z h suc i = suc i t
118 117 eximi t h suc i = s t s suc i t i F z t h suc i = suc i t
119 118 exlimiv s t h suc i = s t s suc i t i F z t h suc i = suc i t
120 111 119 sylbi h suc i suc i × i F z t h suc i = suc i t
121 110 120 syl6bi G h i = suc i × i F z h suc i G h i t h suc i = suc i t
122 103 109 121 sylsyld h : ω ω × A i ω h i = i z k ω h suc k G h k t h suc i = suc i t
123 122 expcom h i = i z h : ω ω × A i ω k ω h suc k G h k t h suc i = suc i t
124 123 exlimiv z h i = i z h : ω ω × A i ω k ω h suc k G h k t h suc i = suc i t
125 124 com3l h : ω ω × A i ω k ω h suc k G h k z h i = i z t h suc i = suc i t
126 opeq2 t = z suc i t = suc i z
127 126 eqeq2d t = z h suc i = suc i t h suc i = suc i z
128 127 cbvexvw t h suc i = suc i t z h suc i = suc i z
129 125 128 syl8ib h : ω ω × A i ω k ω h suc k G h k z h i = i z z h suc i = suc i z
130 129 impancom h : ω ω × A k ω h suc k G h k i ω z h i = i z z h suc i = suc i z
131 130 3adant2 h : ω ω × A h = C k ω h suc k G h k i ω z h i = i z z h suc i = suc i z
132 131 adantl C A h : ω ω × A h = C k ω h suc k G h k i ω z h i = i z z h suc i = suc i z
133 132 com12 i ω C A h : ω ω × A h = C k ω h suc k G h k z h i = i z z h suc i = suc i z
134 68 72 76 81 133 finds2 m ω C A h : ω ω × A h = C k ω h suc k G h k z h m = m z
135 134 com12 C A h : ω ω × A h = C k ω h suc k G h k m ω z h m = m z
136 135 ralrimiv C A h : ω ω × A h = C k ω h suc k G h k m ω z h m = m z
137 fveq2 m = k h m = h k
138 opeq1 m = k m z = k z
139 137 138 eqeq12d m = k h m = m z h k = k z
140 139 exbidv m = k z h m = m z z h k = k z
141 140 rspccv m ω z h m = m z k ω z h k = k z
142 136 141 syl C A h : ω ω × A h = C k ω h suc k G h k k ω z h k = k z
143 142 3impia C A h : ω ω × A h = C k ω h suc k G h k k ω z h k = k z
144 simp21 C A h : ω ω × A h = C k ω h suc k G h k k ω h : ω ω × A
145 simp3 C A h : ω ω × A h = C k ω h suc k G h k k ω k ω
146 rspa k ω h suc k G h k k ω h suc k G h k
147 146 3ad2antl3 h : ω ω × A h = C k ω h suc k G h k k ω h suc k G h k
148 147 3adant1 C A h : ω ω × A h = C k ω h suc k G h k k ω h suc k G h k
149 simpl h k = k z h : ω ω × A k ω h k = k z
150 149 fveq2d h k = k z h : ω ω × A k ω G h k = G k z
151 simprr h k = k z h : ω ω × A k ω k ω
152 eleq1 h k = k z h k ω × A k z ω × A
153 opelxp2 k z ω × A z A
154 152 153 syl6bi h k = k z h k ω × A z A
155 ffvelrn h : ω ω × A k ω h k ω × A
156 154 155 impel h k = k z h : ω ω × A k ω z A
157 df-ov k G z = G k z
158 suceq n = k suc n = suc k
159 158 sneqd n = k suc n = suc k
160 oveq1 n = k n F x = k F x
161 159 160 xpeq12d n = k suc n × n F x = suc k × k F x
162 oveq2 x = z k F x = k F z
163 162 xpeq2d x = z suc k × k F x = suc k × k F z
164 snex suc k V
165 ovex k F z V
166 164 165 xpex suc k × k F z V
167 161 163 2 166 ovmpo k ω z A k G z = suc k × k F z
168 157 167 eqtr3id k ω z A G k z = suc k × k F z
169 151 156 168 syl2anc h k = k z h : ω ω × A k ω G k z = suc k × k F z
170 150 169 eqtrd h k = k z h : ω ω × A k ω G h k = suc k × k F z
171 170 eleq2d h k = k z h : ω ω × A k ω h suc k G h k h suc k suc k × k F z
172 elxp h suc k suc k × k F z s t h suc k = s t s suc k t k F z
173 peano2 k ω suc k ω
174 fvco3 h : ω ω × A suc k ω 2 nd h suc k = 2 nd h suc k
175 173 174 sylan2 h : ω ω × A k ω 2 nd h suc k = 2 nd h suc k
176 175 adantl h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k = 2 nd h suc k
177 simpll h suc k = s t h k = k z h : ω ω × A k ω h suc k = s t
178 177 fveq2d h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k = 2 nd s t
179 176 178 eqtrd h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k = 2 nd s t
180 vex s V
181 vex t V
182 180 181 op2nd 2 nd s t = t
183 179 182 eqtrdi h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k = t
184 fvco3 h : ω ω × A k ω 2 nd h k = 2 nd h k
185 184 adantl h suc k = s t h k = k z h : ω ω × A k ω 2 nd h k = 2 nd h k
186 simplr h suc k = s t h k = k z h : ω ω × A k ω h k = k z
187 186 fveq2d h suc k = s t h k = k z h : ω ω × A k ω 2 nd h k = 2 nd k z
188 185 187 eqtrd h suc k = s t h k = k z h : ω ω × A k ω 2 nd h k = 2 nd k z
189 vex k V
190 vex z V
191 189 190 op2nd 2 nd k z = z
192 188 191 eqtrdi h suc k = s t h k = k z h : ω ω × A k ω 2 nd h k = z
193 192 oveq2d h suc k = s t h k = k z h : ω ω × A k ω k F 2 nd h k = k F z
194 183 193 eleq12d h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k k F 2 nd h k t k F z
195 194 biimprcd t k F z h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k k F 2 nd h k
196 195 exp4c t k F z h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k k F 2 nd h k
197 196 adantl s suc k t k F z h suc k = s t h k = k z h : ω ω × A k ω 2 nd h suc k k F 2 nd h k
198 197 impcom h suc k = s t s suc k t k F z h k = k z h : ω ω × A k ω 2 nd h suc k k F 2 nd h k
199 198 exlimivv s t h suc k = s t s suc k t k F z h k = k z h : ω ω × A k ω 2 nd h suc k k F 2 nd h k
200 172 199 sylbi h suc k suc k × k F z h k = k z h : ω ω × A k ω 2 nd h suc k k F 2 nd h k
201 200 com3l h k = k z h : ω ω × A k ω h suc k suc k × k F z 2 nd h suc k k F 2 nd h k
202 201 imp h k = k z h : ω ω × A k ω h suc k suc k × k F z 2 nd h suc k k F 2 nd h k
203 171 202 sylbid h k = k z h : ω ω × A k ω h suc k G h k 2 nd h suc k k F 2 nd h k
204 203 ex h k = k z h : ω ω × A k ω h suc k G h k 2 nd h suc k k F 2 nd h k
205 204 exlimiv z h k = k z h : ω ω × A k ω h suc k G h k 2 nd h suc k k F 2 nd h k
206 205 3imp z h k = k z h : ω ω × A k ω h suc k G h k 2 nd h suc k k F 2 nd h k
207 143 144 145 148 206 syl121anc C A h : ω ω × A h = C k ω h suc k G h k k ω 2 nd h suc k k F 2 nd h k
208 207 3expia C A h : ω ω × A h = C k ω h suc k G h k k ω 2 nd h suc k k F 2 nd h k
209 64 208 ralrimi C A h : ω ω × A h = C k ω h suc k G h k k ω 2 nd h suc k k F 2 nd h k
210 46 58 209 3jca C A h : ω ω × A h = C k ω h suc k G h k 2 nd h : ω A 2 nd h = C k ω 2 nd h suc k k F 2 nd h k
211 feq1 g = 2 nd h g : ω A 2 nd h : ω A
212 fveq1 g = 2 nd h g = 2 nd h
213 212 eqeq1d g = 2 nd h g = C 2 nd h = C
214 fveq1 g = 2 nd h g suc k = 2 nd h suc k
215 fveq1 g = 2 nd h g k = 2 nd h k
216 215 oveq2d g = 2 nd h k F g k = k F 2 nd h k
217 214 216 eleq12d g = 2 nd h g suc k k F g k 2 nd h suc k k F 2 nd h k
218 217 ralbidv g = 2 nd h k ω g suc k k F g k k ω 2 nd h suc k k F 2 nd h k
219 211 213 218 3anbi123d g = 2 nd h g : ω A g = C k ω g suc k k F g k 2 nd h : ω A 2 nd h = C k ω 2 nd h suc k k F 2 nd h k
220 49 210 219 spcedv C A h : ω ω × A h = C k ω h suc k G h k g g : ω A g = C k ω g suc k k F g k
221 220 ex C A h : ω ω × A h = C k ω h suc k G h k g g : ω A g = C k ω g suc k k F g k
222 221 exlimdv C A h h : ω ω × A h = C k ω h suc k G h k g g : ω A g = C k ω g suc k k F g k
223 222 adantr C A F : ω × A 𝒫 A h h : ω ω × A h = C k ω h suc k G h k g g : ω A g = C k ω g suc k k F g k
224 43 223 mpd C A F : ω × A 𝒫 A g g : ω A g = C k ω g suc k k F g k