Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axdc3lem2 Unicode version

Theorem axdc3lem2 8852
 Description: Lemma for axdc3 8855. We have constructed a "candidate set" , which consists of all finite sequences that satisfy our property of interest, namely (x 1)e. ( (x)) on its domain, but with the added constraint that (0)= . These sets are possible "initial segments" of the infinite sequence satisfying these constraints, but we can leverage the standard ax-dc 8847 (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely (for some integer ). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc 8847 yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that given the sequence , we can construct the sequence that we are after. (Contributed by Mario Carneiro, 30-Jan-2013.)
Hypotheses
Ref Expression
axdc3lem2.1
axdc3lem2.2
axdc3lem2.3
Assertion
Ref Expression
axdc3lem2
Distinct variable groups:   ,,   ,,   ,,,   ,,,   ,,   ,,   ,   S,,   ,S,   ,   ,,

Proof of Theorem axdc3lem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . . . . . . . . 13
2 fveq2 5871 . . . . . . . . . . . . . 14
32dmeqd 5210 . . . . . . . . . . . . 13
41, 3eleq12d 2539 . . . . . . . . . . . 12
5 eleq2 2530 . . . . . . . . . . . . 13
62sseq2d 3531 . . . . . . . . . . . . 13
75, 6imbi12d 320 . . . . . . . . . . . 12
84, 7anbi12d 710 . . . . . . . . . . 11
9 id 22 . . . . . . . . . . . . 13
10 fveq2 5871 . . . . . . . . . . . . . 14
1110dmeqd 5210 . . . . . . . . . . . . 13
129, 11eleq12d 2539 . . . . . . . . . . . 12
13 elequ2 1823 . . . . . . . . . . . . 13
1410sseq2d 3531 . . . . . . . . . . . . 13
1513, 14imbi12d 320 . . . . . . . . . . . 12
1612, 15anbi12d 710 . . . . . . . . . . 11
17 id 22 . . . . . . . . . . . . 13
18 fveq2 5871 . . . . . . . . . . . . . 14
1918dmeqd 5210 . . . . . . . . . . . . 13
2017, 19eleq12d 2539 . . . . . . . . . . . 12
21 eleq2 2530 . . . . . . . . . . . . 13
2218sseq2d 3531 . . . . . . . . . . . . 13
2321, 22imbi12d 320 . . . . . . . . . . . 12
2420, 23anbi12d 710 . . . . . . . . . . 11
25 peano1 6719 . . . . . . . . . . . . . . 15
26 ffvelrn 6029 . . . . . . . . . . . . . . 15
2725, 26mpan2 671 . . . . . . . . . . . . . 14
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18
29 fdm 5740 . . . . . . . . . . . . . . . . . . . . . . 23
30 nnord 6708 . . . . . . . . . . . . . . . . . . . . . . . . 25
31 0elsuc 6670 . . . . . . . . . . . . . . . . . . . . . . . . 25
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
33 peano2 6720 . . . . . . . . . . . . . . . . . . . . . . . 24
34 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . 26
35 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3634, 35anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . 25
3736biimprcd 225 . . . . . . . . . . . . . . . . . . . . . . . 24
3832, 33, 37syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
3929, 38syl5com 30 . . . . . . . . . . . . . . . . . . . . . 22
40393ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . 21
4140impcom 430 . . . . . . . . . . . . . . . . . . . 20
4241rexlimiva 2945 . . . . . . . . . . . . . . . . . . 19
4342ss2abi 3571 . . . . . . . . . . . . . . . . . 18
4428, 43eqsstri 3533 . . . . . . . . . . . . . . . . 17
4544sseli 3499 . . . . . . . . . . . . . . . 16
46 fvex 5881 . . . . . . . . . . . . . . . . 17
47 dmeq 5208 . . . . . . . . . . . . . . . . . . 19
4847eleq2d 2527 . . . . . . . . . . . . . . . . . 18
4947eleq1d 2526 . . . . . . . . . . . . . . . . . 18
5048, 49anbi12d 710 . . . . . . . . . . . . . . . . 17
5146, 50elab 3246 . . . . . . . . . . . . . . . 16
5245, 51sylib 196 . . . . . . . . . . . . . . 15
5352simpld 459 . . . . . . . . . . . . . 14
5427, 53syl 16 . . . . . . . . . . . . 13
55 noel 3788 . . . . . . . . . . . . . 14
5655pm2.21i 131 . . . . . . . . . . . . 13
5754, 56jctir 538 . . . . . . . . . . . 12
5857adantr 465 . . . . . . . . . . 11
59 ffvelrn 6029 . . . . . . . . . . . . . . 15
6059ancoms 453 . . . . . . . . . . . . . 14
6160adantrr 716 . . . . . . . . . . . . 13
62 suceq 4948 . . . . . . . . . . . . . . . . 17
6362fveq2d 5875 . . . . . . . . . . . . . . . 16
64 fveq2 5871 . . . . . . . . . . . . . . . . 17
6564fveq2d 5875 . . . . . . . . . . . . . . . 16
6663, 65eleq12d 2539 . . . . . . . . . . . . . . 15
6766rspcva 3208 . . . . . . . . . . . . . 14
6867adantrl 715 . . . . . . . . . . . . 13
6944sseli 3499 . . . . . . . . . . . . . . . . . . . 20
70 fvex 5881 . . . . . . . . . . . . . . . . . . . . 21
71 dmeq 5208 . . . . . . . . . . . . . . . . . . . . . . 23
7271eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . 22
7371eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . 22
7472, 73anbi12d 710 . . . . . . . . . . . . . . . . . . . . 21
7570, 74elab 3246 . . . . . . . . . . . . . . . . . . . 20
7669, 75sylib 196 . . . . . . . . . . . . . . . . . . 19
7776simprd 463 . . . . . . . . . . . . . . . . . 18
78 nnord 6708 . . . . . . . . . . . . . . . . . 18
79 ordsucelsuc 6657 . . . . . . . . . . . . . . . . . 18
8077, 78, 793syl 20 . . . . . . . . . . . . . . . . 17
8180adantr 465 . . . . . . . . . . . . . . . 16
82 dmeq 5208 . . . . . . . . . . . . . . . . . . . . . . . . . 26
83 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8482, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
8584eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . 24
8682reseq2d 5278 . . . . . . . . . . . . . . . . . . . . . . . . 25
87 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25
8886, 87eqeq12d 2479 . . . . . . . . . . . . . . . . . . . . . . . 24
8985, 88anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . 23
9089rabbidv 3101 . . . . . . . . . . . . . . . . . . . . . 22
91 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22
92 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24
9392, 28axdc3lem 8851 . . . . . . . . . . . . . . . . . . . . . . 23
9493rabex 4603 . . . . . . . . . . . . . . . . . . . . . 22
9590, 91, 94fvmpt 5956 . . . . . . . . . . . . . . . . . . . . 21
9695eleq2d 2527 . . . . . . . . . . . . . . . . . . . 20
97 dmeq 5208 . . . . . . . . . . . . . . . . . . . . . . 23
9897eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . 22
99 reseq1 5272 . . . . . . . . . . . . . . . . . . . . . . 23
10099eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . 22
10198, 100anbi12d 710 . . . . . . . . . . . . . . . . . . . . 21
102101elrab 3257 . . . . . . . . . . . . . . . . . . . 20
10396, 102syl6bb 261 . . . . . . . . . . . . . . . . . . 19
104103simplbda 624 . . . . . . . . . . . . . . . . . 18
105104simpld 459 . . . . . . . . . . . . . . . . 17
106105eleq2d 2527 . . . . . . . . . . . . . . . 16
10781, 106bitr4d 256 . . . . . . . . . . . . . . 15
108107biimpd 207 . . . . . . . . . . . . . 14
109104simprd 463 . . . . . . . . . . . . . . 15
110 resss 5302 . . . . . . . . . . . . . . . 16
111 sseq1 3524 . . . . . . . . . . . . . . . 16
112110, 111mpbii 211 . . . . . . . . . . . . . . 15
113 elsuci 4949 . . . . . . . . . . . . . . . . 17
114 pm2.27 39 . . . . . . . . . . . . . . . . . . 19
115 sstr2 3510 . . . . . . . . . . . . . . . . . . 19
116114, 115syl6 33 . . . . . . . . . . . . . . . . . 18
117 fveq2 5871 . . . . . . . . . . . . . . . . . . . . 21
118117sseq1d 3530 . . . . . . . . . . . . . . . . . . . 20
119118biimprd 223 . . . . . . . . . . . . . . . . . . 19
120119a1d 25 . . . . . . . . . . . . . . . . . 18
121116, 120jaoi 379 . . . . . . . . . . . . . . . . 17
122113, 121syl 16 . . . . . . . . . . . . . . . 16
123122com13 80 . . . . . . . . . . . . . . 15
124109, 112, 1233syl 20 . . . . . . . . . . . . . 14
125108, 124anim12d 563 . . . . . . . . . . . . 13
12661, 68, 125syl2anc 661 . . . . . . . . . . . 12
127126ex 434 . . . . . . . . . . 11
1288, 16, 24, 58, 127finds2 6728 . . . . . . . . . 10
129128imp 429 . . . . . . . . 9
130129simprd 463 . . . . . . . 8
131130expcom 435 . . . . . . 7
132131ralrimdv 2873 . . . . . 6
133132ralrimiv 2869 . . . . 5
134 frn 5742 . . . . . . . . . . . 12
135 ffun 5738 . . . . . . . . . . . . . . . 16
1361353ad2ant1 1017 . . . . . . . . . . . . . . 15
137136rexlimivw 2946 . . . . . . . . . . . . . 14
138137ss2abi 3571 . . . . . . . . . . . . 13
13928, 138eqsstri 3533 . . . . . . . . . . . 12
140134, 139syl6ss 3515 . . . . . . . . . . 11
141140sseld 3502 . . . . . . . . . 10
142 vex 3112 . . . . . . . . . . 11
143 funeq 5612 . . . . . . . . . . 11
144142, 143elab 3246 . . . . . . . . . 10
145141, 144syl6ib 226 . . . . . . . . 9
146145adantr 465 . . . . . . . 8
147 ffn 5736 . . . . . . . . 9
148 fvelrnb 5920 . . . . . . . . . . . . 13
149 fvelrnb 5920 . . . . . . . . . . . . . . 15
150 nnord 6708 . . . . . . . . . . . . . . . . . . . . . . 23
151 nnord 6708 . . . . . . . . . . . . . . . . . . . . . . 23
152150, 151anim12i 566 . . . . . . . . . . . . . . . . . . . . . 22
153 ordtri3or 4915 . . . . . . . . . . . . . . . . . . . . . . 23
154 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155154sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156155raleqbi1dv 3062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157156rspcv 3206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
159158sseq1d 3530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160159rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161157, 160syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162161adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1631623imp 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
164163orcd 392 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1651643exp 1195 . . . . . . . . . . . . . . . . . . . . . . . . 25
166165com3r 79 . . . . . . . . . . . . . . . . . . . . . . . 24
167 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
168 eqimss 3555 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
169168orcd 392 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
170167, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
171170a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . 25
172171a1d 25 . . . . . . . . . . . . . . . . . . . . . . . 24
173 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
174173sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
175174raleqbi1dv 3062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
176175rspcv 3206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
177 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178177sseq1d 3530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179178rspccv 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180176, 179syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
181180adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1821813imp 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
183182olcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . 26
1841833exp 1195 . . . . . . . . . . . . . . . . . . . . . . . . 25
185184com3r 79 . . . . . . . . . . . . . . . . . . . . . . . 24
186166, 172, 1853jaoi 1291 . . . . . . . . . . . . . . . . . . . . . . 23
187153, 186syl 16 . . . . . . . . . . . . . . . . . . . . . 22
188152, 187mpcom 36 . . . . . . . . . . . . . . . . . . . . 21
189 sseq12 3526 . . . . . . . . . . . . . . . . . . . . . . 23
190 sseq12 3526 . . . . . . . . . . . . . . . . . . . . . . . 24
191190ancoms 453 . . . . . . . . . . . . . . . . . . . . . . 23
192189, 191orbi12d 709 . . . . . . . . . . . . . . . . . . . . . 22