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

Theorem axdc3lem4 8854
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 is nonempty, and that always maps to a nonempty subset of , so that we can apply axdc2 8850. See axdc3lem2 8852 for the rest of the proof. (Contributed by Mario Carneiro, 27-Jan-2013.)
Hypotheses
Ref Expression
axdc3lem4.1
axdc3lem4.2
axdc3lem4.3
Assertion
Ref Expression
axdc3lem4
Distinct variable groups:   , ,   , , , ,   , ,   , ,   , ,   , , ,   ,   S, , ,   ,S,   ,

Proof of Theorem axdc3lem4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 6719 . . . . . 6
2 eqid 2457 . . . . . . . . . 10
3 fsng 6070 . . . . . . . . . . 11
41, 3mpan 670 . . . . . . . . . 10
52, 4mpbiri 233 . . . . . . . . 9
6 snssi 4174 . . . . . . . . 9
75, 6fssd 5745 . . . . . . . 8
8 suc0 4957 . . . . . . . . 9
98feq2i 5729 . . . . . . . 8
107, 9sylibr 212 . . . . . . 7
11 fvsng 6105 . . . . . . . 8
121, 11mpan 670 . . . . . . 7
13 ral0 3934 . . . . . . . 8
1413a1i 11 . . . . . . 7
1510, 12, 143jca 1176 . . . . . 6
16 suceq 4948 . . . . . . . . 9
1716feq2d 5723 . . . . . . . 8
18 raleq 3054 . . . . . . . 8
1917, 183anbi13d 1301 . . . . . . 7
2019rspcev 3210 . . . . . 6
211, 15, 20sylancr 663 . . . . 5
22 axdc3lem4.1 . . . . . 6
23 axdc3lem4.2 . . . . . 6
24 snex 4693 . . . . . 6
2522, 23, 24axdc3lem3 8853 . . . . 5
2621, 25sylibr 212 . . . 4
27 ne0i 3790 . . . 4
2826, 27syl 16 . . 3
29 ssrab2 3584 . . . . . . 7
3022, 23axdc3lem 8851 . . . . . . . 8
3130elpw2 4616 . . . . . . 7
3229, 31mpbir 209 . . . . . 6
3332a1i 11 . . . . 5
34 vex 3112 . . . . . . . . . 10
3522, 23, 34axdc3lem3 8853 . . . . . . . . 9
36 simp2 997 . . . . . . . . . . . . . . . 16
37 vex 3112 . . . . . . . . . . . . . . . . . . . . . 22
3837sucid 4962 . . . . . . . . . . . . . . . . . . . . 21
39 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . 21
4038, 39mpan2 671 . . . . . . . . . . . . . . . . . . . 20
41 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . 20
4240, 41sylan2 474 . . . . . . . . . . . . . . . . . . 19
43 eldifn 3626 . . . . . . . . . . . . . . . . . . . 20
44 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . 23
4544elsnc 4053 . . . . . . . . . . . . . . . . . . . . . 22
4645necon3bbii 2718 . . . . . . . . . . . . . . . . . . . . 21
47 n0 3794 . . . . . . . . . . . . . . . . . . . . 21
4846, 47bitri 249 . . . . . . . . . . . . . . . . . . . 20
4943, 48sylib 196 . . . . . . . . . . . . . . . . . . 19
5042, 49syl 16 . . . . . . . . . . . . . . . . . 18
51 simp32 1033 . . . . . . . . . . . . . . . . . . . . . . . 24
52 eldifi 3625 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
53 elelpwi 4023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5453expcom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5542, 52, 543syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
56 peano2 6720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
57563ad2ant3 1019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
58573ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
59 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6034dmex 6733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
61 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
62 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
63 fsng 6070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
6462, 63mpbiri 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
6560, 61, 64mp2an 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
66 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
6766snssd 4175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
68 fss 5744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
6965, 67, 68sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
70 fdm 5740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
7156adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
72 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
7372adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
7471, 73mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
75 nnord 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
76 ordirr 4901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
7774, 75, 763syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
78 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
7978adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
8077, 79mtbid 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
81 disjsn 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
8280, 81sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
8370, 82sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
8483adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
85 fun2 5754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
8659, 69, 84, 85syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
87 sneq 4039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
8887uneq2d 3657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
89 df-suc 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
9088, 89syl6eqr 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
9170, 90syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
9291ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
9392feq2d 5723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
9486, 93mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9594ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9695adantrd 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9796a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9897ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
99983adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
100993imp 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
101 ffun 5738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
102101adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
10360, 61funsn 5641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
104102, 103jctir 538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
10561dmsnop 5487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
106105ineq2i 3696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
107 disjsn 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
10877, 107sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
109106, 108syl5eq 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
11070, 109sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
111 funun 5635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
112104, 110, 111syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
113 ssun1 3666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
115 nnord 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
116 0elsuc 6670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
117115, 116syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
118117adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
11970eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
120119adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
121118, 120mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
122 funssfv 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
123112, 114, 121, 122syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
124123eqeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
125124ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1261253adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
127126biimpar 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
128127adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1291283adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
130 nfra1 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
131 nfv 1707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
132 nfv 1707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
133130, 131, 132nf3an 1930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
134 nfv 1707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
135 nfv 1707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
136133, 134, 135nf3an 1930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
137 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
138 elsuci 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
139 rsp 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
140139impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
141140ad2ant2lr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
1421413adant3 1016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
143112adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
144113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
145 ordsucelsuc 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
146115, 145syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
147146biimpa 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
148 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
149148biimparc 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
150147, 70, 149syl2an 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
151 funssfv 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
152143, 144, 150, 151syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
1531523adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
1541123adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
155113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
156 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
157156biimparc 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
15870, 157sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1591583adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
160 funssfv 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
161154, 155, 159, 160syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
1621613adant1r 1221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
163162fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
164153, 163eleq12d 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
1651643adant2l 1222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
166142, 165mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
167166a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
1681673expib 1199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
169168expcom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
1701123adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
171 ssun2 3667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
173 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
174173eqeq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
175174biimpar 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
17660snid 4057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
177176, 105eleqtrri 2544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
178175, 177syl6eqelr 2554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
17970, 178sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1801793adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
181 funssfv 5886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
182170, 172, 180, 181syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
1831753adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
18460, 61fvsn 6104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
185 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
186184, 185syl5reqr 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
187183, 186syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
18870, 187syl3an3 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
189182, 188eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51