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

Theorem axdc3lem4 8334
 Description: Lemma for axdc3 8335. We have constructed a "candidate set" , which consists of all finite sequences that satisfy our property of interest, namely on its domain, but with the added constraint that . These sets are possible "initial segments" of the infinite sequence satisfying these constraints, but we can leverage the standard ax-dc 8327 (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 8327 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 8330. See axdc3lem2 8332 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:   ,,   ,,,,   ,,   ,,   ,,   ,,,   ,   ,,,   ,,   ,
Allowed substitution hints:   ()   (,)   (,)   ()   (,,,,)

Proof of Theorem axdc3lem4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 4865 . . . . . 6
2 eqid 2437 . . . . . . . . . 10
3 fsng 5908 . . . . . . . . . . 11
41, 3mpan 653 . . . . . . . . . 10
52, 4mpbiri 226 . . . . . . . . 9
6 snssi 3943 . . . . . . . . 9
7 fss 5600 . . . . . . . . 9
85, 6, 7syl2anc 644 . . . . . . . 8
9 suc0 4656 . . . . . . . . 9
109feq2i 5587 . . . . . . . 8
118, 10sylibr 205 . . . . . . 7
12 fvsng 5928 . . . . . . . 8
131, 12mpan 653 . . . . . . 7
14 ral0 3733 . . . . . . . 8
1514a1i 11 . . . . . . 7
1611, 13, 153jca 1135 . . . . . 6
17 suceq 4647 . . . . . . . . 9
1817feq2d 5582 . . . . . . . 8
19 raleq 2905 . . . . . . . 8
2018, 193anbi13d 1257 . . . . . . 7
2120rspcev 3053 . . . . . 6
221, 16, 21sylancr 646 . . . . 5
23 axdc3lem4.1 . . . . . 6
24 axdc3lem4.2 . . . . . 6
25 snex 4406 . . . . . 6
2623, 24, 25axdc3lem3 8333 . . . . 5
2722, 26sylibr 205 . . . 4
28 ne0i 3635 . . . 4
2927, 28syl 16 . . 3
30 ssrab2 3429 . . . . . . 7
3123, 24axdc3lem 8331 . . . . . . . 8
3231elpw2 4365 . . . . . . 7
3330, 32mpbir 202 . . . . . 6
3433a1i 11 . . . . 5
35 vex 2960 . . . . . . . . . 10
3623, 24, 35axdc3lem3 8333 . . . . . . . . 9
37 simp2 959 . . . . . . . . . . . . . . . 16
38 vex 2960 . . . . . . . . . . . . . . . . . . . . . 22
3938sucid 4661 . . . . . . . . . . . . . . . . . . . . 21
40 ffvelrn 5869 . . . . . . . . . . . . . . . . . . . . 21
4139, 40mpan2 654 . . . . . . . . . . . . . . . . . . . 20
42 ffvelrn 5869 . . . . . . . . . . . . . . . . . . . 20
4341, 42sylan2 462 . . . . . . . . . . . . . . . . . . 19
44 eldifn 3471 . . . . . . . . . . . . . . . . . . . 20
45 fvex 5743 . . . . . . . . . . . . . . . . . . . . . . 23
4645elsnc 3838 . . . . . . . . . . . . . . . . . . . . . 22
4746necon3bbii 2633 . . . . . . . . . . . . . . . . . . . . 21
48 n0 3638 . . . . . . . . . . . . . . . . . . . . 21
4947, 48bitri 242 . . . . . . . . . . . . . . . . . . . 20
5044, 49sylib 190 . . . . . . . . . . . . . . . . . . 19
5143, 50syl 16 . . . . . . . . . . . . . . . . . 18
52 simp32 995 . . . . . . . . . . . . . . . . . . . . . . . 24
53 eldifi 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
54 elelpwi 3810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5554expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5643, 53, 553syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
57 peano2 4866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
58573ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
59583ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
60 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
6135dmex 5133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
62 vex 2960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
63 eqid 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
64 fsng 5908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
6563, 64mpbiri 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
6661, 62, 65mp2an 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
67 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
6867snssd 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
69 fss 5600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
7066, 68, 69sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
71 fdm 5596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
7257adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
73 eleq1 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
7473adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
7572, 74mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
76 nnord 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
77 ordirr 4600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
7875, 76, 773syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
79 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
8079adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
8178, 80mtbid 293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
82 disjsn 3869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
8381, 82sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
8471, 83sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
8584adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
86 fun2 5609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
8760, 70, 85, 86syl21anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
88 sneq 3826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
8988uneq2d 3502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
90 df-suc 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
9189, 90syl6eqr 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
9271, 91syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
9392ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
9493feq2d 5582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
9587, 94mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9695ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9796adantrd 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9897a1d 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
9998ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
100993adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1011003imp 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
102 ffun 5594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
103102adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
10461, 62funsn 5500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
105103, 104jctir 526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
10662dmsnop 5345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
107106ineq2i 3540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
108 disjsn 3869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
10978, 108sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
110107, 109syl5eq 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
11171, 110sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
112 funun 5496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
113105, 111, 112syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
114 ssun1 3511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
115114a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
116 nnord 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
117 0elsuc 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
118116, 117syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
119118adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
12071eleq2d 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
121120adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
122119, 121mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
123 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
124113, 115, 122, 123syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
125124eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
126125ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1271263adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
128127biimpar 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
129128adantrl 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1301293adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
131 nfra1 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
132 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
133 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
134131, 132, 133nf3an 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
135 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
136 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
137134, 135, 136nf3an 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
138 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
139 elsuci 4648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
140 rsp 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
141140impcom 421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
142141ad2ant2lr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
1431423adant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
144113adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
145114a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
146 ordsucelsuc 4803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
147116, 146syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
148147biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
149 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
150149biimparc 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
151148, 71, 150syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
152 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
153144, 145, 151, 152syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
1541533adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
1551133adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
156114a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
157 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
158157biimparc 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
15971, 158sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1601593adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
161 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
162155, 156, 160, 161syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
1631623adant1r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
164163fveq2d 5733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
165154, 164eleq12d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
1661653adant2l 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
167143, 166mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
168167a1d 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
1691683expib 1157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
170169expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
1711133adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
172 ssun2 3512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
173172a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
174 suceq 4647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
175174eqeq2d 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
176175biimpar 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
17761snid 3842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
178177, 106eleqtrri 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
179176, 178syl6eqelr 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
18071, 179sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
1811803adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
182 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
183171, 173, 181, 182syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
1841763adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
18561, 62fvsn 5927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
186 fveq2 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
187185, 186syl5reqr 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
188184, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
18971, 188syl3an3 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
190183, 189eqtrd 2469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
1911903expa 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
1921913adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
1931623adant1l 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
194 fveq2 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
195194adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
1961953ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
197193, 196eqtrd 2469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
198197fveq2d 5733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
199192, 198eleq12d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
2001993adant2l 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
201200biimprd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
2022013expib 1157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
203202ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
204170, 203jaoi 370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
205139, 204syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
206205com3r 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
207138, 206mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
208207ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
209208expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
2102093impd 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
211210imp3a 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
212211com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
2132123adant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
214137, 213ralrimi 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
215 suceq 4647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
216215feq2d 5582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
217 raleq 2905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
218216, 2173anbi13d 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
219218rspcev 3053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
22059, 101, 130, 214, 219syl13anc 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
221 snex 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
22235, 221unex 4708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
22323, 24, 222axdc3lem3 8333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
224220, 223sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2252243coml 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2262253exp 1153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
227226exp3a 427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
22856, 227sylcom 28 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2292283impd 1168 . . . . . . . . . . . . . . . . . . . . . . . . . 26
230229ex 425 . . . . . . . . . . . . . . . . . . . . . . . . 25
231230com23 75 . . . . . . . . . . . . . . . . . . . . . . . 24
23252, 231mpdi 41 . . . . . . . . . . . . . . . . . . . . . . 23
233232imp 420 . . . . . . . . . . . . . . . . . . . . . 22
234 resundir 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
235 frel 5595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
236 resdm 5185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
237235, 236syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
238237adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
23971, 75sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
24076, 77syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
241 incom 3534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242241eqeq1i 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
24361, 62fnsn 5505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
244 fnresdisj 5556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
245243, 244ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
246242, 245, 1083bitr3ri 269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
247240, 246sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
248239, 247syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
249238, 248uneq12d 3503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
250 un0 3653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
251249, 250syl6eq 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
252234, 251syl5eq 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
253252ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2542533adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . 25
2552543ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . 24
256255adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23
257106uneq2i 3499 . . . . . . . . . . . . . . . . . . . . . . . 24
258 dmun 5077 . . . . . . . . . . . . . . . . . . . . . . . 24
259 df-suc 4588 . . . . . . . . . . . . . . . . . . . . . . . 24
260257, 258, 2593eqtr4i 2467 . . . . . . . . . . . . . . . . . . . . . . 23
261256, 260jctil 525 . . . . . . . . . . . . . . . . . . . . . 22
262 dmeq 5071 . . . . . . . . . . . . . . . . . . . . . . . . 25
263262eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . 24
264 reseq1 5141 . . . . . . . . . . . . . . . . . . . . . . . . 25
265264eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . 24
266263, 265anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . 23
267266rspcev 3053 . . . . . . . . . . . . . . . . . . . . . 22
268233, 261, 267syl2anc 644 . . . . . . . . . . . . . . . . . . . . 21
2692683exp2 1172 . . . . . . . . . . . . . . . . . . . 20
270269exlimdv 1647 . . . . . . . . . . . . . . . . . . 19
271270adantr 453 . . . . . . . . . . . . . . . . . 18
27251, 271mpd 15 . . . . . . . . . . . . . . . . 17
273272com3r 76 . . . . . . . . . . . . . . . 16
27437, 273mpan2d 657 . . . . . . . . . . . . . . 15
275274com3r 76 . . . . . . . . . . . . . 14
2762753expd 1171 . . . . . . . . . . . . 13
277276com3r 76 . . . . . . . . . . . 12
2782773imp 1148 . . . . . . . . . . 11
279278com12 30 . . . . . . . . . 10
280279rexlimiv 2825 . . . . . . . . 9
28136, 280sylbi 189 . . . . . . . 8
282281impcom 421 . . . . . . 7
283 rabn0 3648 . . . . . . 7
284282, 283sylibr 205 . . . . . 6
28531rabex 4355 . . . . . . . 8
286285elsnc 3838 . . . . . . 7
287286necon3bbii 2633 . . . . . 6
288284, 287sylibr 205 . . . . 5
28934, 288eldifd 3332 . . . 4
290 axdc3lem4.3 . . . 4
291289, 290fmptd 5894 . . 3
29231axdc2 8330 . . 3
29329, 291, 292syl2an 465 . 2
29423, 24, 290axdc3lem2 8332 . 2
295293, 294syl 16 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wo 359   wa 360   w3a 937  wex 1551   wceq 1653   wcel 1726  cab 2423   wne 2600  wral 2706  wrex 2707  crab 2710  cvv 2957   cdif 3318   cun 3319   cin 3320   wss 3321  c0 3629  cpw 3800  csn 3815  cop 3818   cmpt 4267   word 4581   csuc 4584  com 4846   cdm 4879   cres 4881   wrel 4884   wfun 5449   wfn 5450  wf 5451  cfv 5455 This theorem is referenced by:  axdc3  8335 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-dc 8327 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-1o 6725
 Copyright terms: Public domain W3C validator