Step | Hyp | Ref
| Expression |
1 | | elfznn 11743 |
. . . . . . . 8
|
2 | 1 | a1i 11 |
. . . . . . 7
|
3 | | cnvimass 5362 |
. . . . . . . . 9
|
4 | | isercoll.g |
. . . . . . . . . . 11
|
5 | 4 | adantr 465 |
. . . . . . . . . 10
|
6 | | fdm 5740 |
. . . . . . . . . 10
|
7 | 5, 6 | syl 16 |
. . . . . . . . 9
|
8 | 3, 7 | syl5sseq 3551 |
. . . . . . . 8
|
9 | 8 | sseld 3502 |
. . . . . . 7
|
10 | | id 22 |
. . . . . . . . . . 11
|
11 | | nnuz 11145 |
. . . . . . . . . . 11
|
12 | 10, 11 | syl6eleq 2555 |
. . . . . . . . . 10
|
13 | | ltso 9686 |
. . . . . . . . . . . . . 14
|
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
|
15 | | fzfid 12083 |
. . . . . . . . . . . . . . 15
|
16 | | ffun 5738 |
. . . . . . . . . . . . . . . . 17
|
17 | | funimacnv 5665 |
. . . . . . . . . . . . . . . . 17
|
18 | 5, 16, 17 | 3syl 20 |
. . . . . . . . . . . . . . . 16
|
19 | | inss1 3717 |
. . . . . . . . . . . . . . . 16
|
20 | 18, 19 | syl6eqss 3553 |
. . . . . . . . . . . . . . 15
|
21 | | ssfi 7760 |
. . . . . . . . . . . . . . 15
|
22 | 15, 20, 21 | syl2anc 661 |
. . . . . . . . . . . . . 14
|
23 | | ssid 3522 |
. . . . . . . . . . . . . . . . . . . . 21
|
24 | | isercoll.z |
. . . . . . . . . . . . . . . . . . . . . 22
|
25 | | isercoll.m |
. . . . . . . . . . . . . . . . . . . . . 22
|
26 | | isercoll.i |
. . . . . . . . . . . . . . . . . . . . . 22
|
27 | 24, 25, 4, 26 | isercolllem1 13487 |
. . . . . . . . . . . . . . . . . . . . 21
|
28 | 23, 27 | mpan2 671 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | | ffn 5736 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | | fnresdm 5695 |
. . . . . . . . . . . . . . . . . . . . 21
|
31 | | isoeq1 6215 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 4, 29, 30, 31 | 4syl 21 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 28, 32 | mpbid 210 |
. . . . . . . . . . . . . . . . . . 19
|
34 | | isof1o 6221 |
. . . . . . . . . . . . . . . . . . 19
|
35 | | f1ocnv 5833 |
. . . . . . . . . . . . . . . . . . 19
|
36 | | f1ofun 5823 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 33, 34, 35, 36 | 4syl 21 |
. . . . . . . . . . . . . . . . . 18
|
38 | | df-f1 5598 |
. . . . . . . . . . . . . . . . . 18
|
39 | 4, 37, 38 | sylanbrc 664 |
. . . . . . . . . . . . . . . . 17
|
40 | 39 | adantr 465 |
. . . . . . . . . . . . . . . 16
|
41 | | nnex 10567 |
. . . . . . . . . . . . . . . . 17
|
42 | | ssexg 4598 |
. . . . . . . . . . . . . . . . 17
|
43 | 8, 41, 42 | sylancl 662 |
. . . . . . . . . . . . . . . 16
|
44 | | f1imaeng 7595 |
. . . . . . . . . . . . . . . 16
|
45 | 40, 8, 43, 44 | syl3anc 1228 |
. . . . . . . . . . . . . . 15
|
46 | 45 | ensymd 7586 |
. . . . . . . . . . . . . 14
|
47 | | enfii 7757 |
. . . . . . . . . . . . . 14
|
48 | 22, 46, 47 | syl2anc 661 |
. . . . . . . . . . . . 13
|
49 | | 1nn 10572 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
|
51 | | ffvelrn 6029 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 4, 49, 51 | sylancl 662 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52, 24 | syl6eleq 2555 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | adantr 465 |
. . . . . . . . . . . . . . . 16
|
55 | | simpr 461 |
. . . . . . . . . . . . . . . 16
|
56 | | elfzuzb 11711 |
. . . . . . . . . . . . . . . 16
|
57 | 54, 55, 56 | sylanbrc 664 |
. . . . . . . . . . . . . . 15
|
58 | 5, 29 | syl 16 |
. . . . . . . . . . . . . . . 16
|
59 | | elpreima 6007 |
. . . . . . . . . . . . . . . 16
|
60 | 58, 59 | syl 16 |
. . . . . . . . . . . . . . 15
|
61 | 50, 57, 60 | mpbir2and 922 |
. . . . . . . . . . . . . 14
|
62 | | ne0i 3790 |
. . . . . . . . . . . . . 14
|
63 | 61, 62 | syl 16 |
. . . . . . . . . . . . 13
|
64 | | nnssre 10565 |
. . . . . . . . . . . . . 14
|
65 | 8, 64 | syl6ss 3515 |
. . . . . . . . . . . . 13
|
66 | | fisupcl 7948 |
. . . . . . . . . . . . 13
|
67 | 14, 48, 63, 65, 66 | syl13anc 1230 |
. . . . . . . . . . . 12
|
68 | 8, 67 | sseldd 3504 |
. . . . . . . . . . 11
|
69 | 68 | nnzd 10993 |
. . . . . . . . . 10
|
70 | | elfz5 11709 |
. . . . . . . . . 10
|
71 | 12, 69, 70 | syl2anr 478 |
. . . . . . . . 9
|
72 | | elpreima 6007 |
. . . . . . . . . . . . . . . . . 18
|
73 | 58, 72 | syl 16 |
. . . . . . . . . . . . . . . . 17
|
74 | 67, 73 | mpbid 210 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | simprd 463 |
. . . . . . . . . . . . . . 15
|
76 | | elfzle2 11719 |
. . . . . . . . . . . . . . 15
|
77 | 75, 76 | syl 16 |
. . . . . . . . . . . . . 14
|
78 | 77 | adantr 465 |
. . . . . . . . . . . . 13
|
79 | | uzssz 11129 |
. . . . . . . . . . . . . . . . 17
|
80 | 24, 79 | eqsstri 3533 |
. . . . . . . . . . . . . . . 16
|
81 | | zssre 10896 |
. . . . . . . . . . . . . . . 16
|
82 | 80, 81 | sstri 3512 |
. . . . . . . . . . . . . . 15
|
83 | 5 | ffvelrnda 6031 |
. . . . . . . . . . . . . . 15
|
84 | 82, 83 | sseldi 3501 |
. . . . . . . . . . . . . 14
|
85 | 5, 68 | ffvelrnd 6032 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | adantr 465 |
. . . . . . . . . . . . . . 15
|
87 | 82, 86 | sseldi 3501 |
. . . . . . . . . . . . . 14
|
88 | | eluzelz 11119 |
. . . . . . . . . . . . . . . 16
|
89 | 88 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
|
90 | 81, 89 | sseldi 3501 |
. . . . . . . . . . . . . 14
|
91 | | letr 9699 |
. . . . . . . . . . . . . 14
|
92 | 84, 87, 90, 91 | syl3anc 1228 |
. . . . . . . . . . . . 13
|
93 | 78, 92 | mpan2d 674 |
. . . . . . . . . . . 12
|
94 | 33 | ad2antrr 725 |
. . . . . . . . . . . . 13
|
95 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
|
96 | | ressxr 9658 |
. . . . . . . . . . . . . 14
|
97 | 95, 96 | syl6ss 3515 |
. . . . . . . . . . . . 13
|
98 | | imassrn 5353 |
. . . . . . . . . . . . . . . 16
|
99 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
|
100 | | frn 5742 |
. . . . . . . . . . . . . . . . 17
|
101 | 99, 100 | syl 16 |
. . . . . . . . . . . . . . . 16
|
102 | 98, 101 | syl5ss 3514 |
. . . . . . . . . . . . . . 15
|
103 | 102, 82 | syl6ss 3515 |
. . . . . . . . . . . . . 14
|
104 | 103, 96 | syl6ss 3515 |
. . . . . . . . . . . . 13
|
105 | | simpr 461 |
. . . . . . . . . . . . 13
|
106 | 68 | adantr 465 |
. . . . . . . . . . . . 13
|
107 | | leisorel 12509 |
. . . . . . . . . . . . 13
|
108 | 94, 97, 104, 105, 106, 107 | syl122anc 1237 |
. . . . . . . . . . . 12
|
109 | 83, 24 | syl6eleq 2555 |
. . . . . . . . . . . . 13
|
110 | | elfz5 11709 |
. . . . . . . . . . . . 13
|
111 | 109, 89, 110 | syl2anc 661 |
. . . . . . . . . . . 12
|
112 | 93, 108, 111 | 3imtr4d 268 |
. . . . . . . . . . 11
|
113 | | elpreima 6007 |
. . . . . . . . . . . . 13
|
114 | 113 | baibd 909 |
. . . . . . . . . . . 12
|
115 | 58, 114 | sylan 471 |
. . . . . . . . . . 11
|
116 | 112, 115 | sylibrd 234 |
. . . . . . . . . 10
|
117 | | fimaxre2 10516 |
. . . . . . . . . . . . 13
|
118 | 65, 48, 117 | syl2anc 661 |
. . . . . . . . . . . 12
|
119 | | suprub 10529 |
. . . . . . . . . . . . 13
|
120 | 119 | ex 434 |
. . . . . . . . . . . 12
|
121 | 65, 63, 118, 120 | syl3anc 1228 |
. . . . . . . . . . 11
|
122 | 121 | adantr 465 |
. . . . . . . . . 10
|
123 | 116, 122 | impbid 191 |
. . . . . . . . 9
|
124 | 71, 123 | bitrd 253 |
. . . . . . . 8
|
125 | 124 | ex 434 |
. . . . . . 7
|
126 | 2, 9, 125 | pm5.21ndd 354 |
. . . . . 6
|
127 | 126 | eqrdv 2454 |
. . . . 5
|
128 | 127 | fveq2d 5875 |
. . . 4
|
129 | 68 | nnnn0d 10877 |
. . . . 5
|
130 | | hashfz1 12419 |
. . . . 5
|
131 | 129, 130 | syl 16 |
. . . 4
|
132 | | hashen 12420 |
. . . . . 6
|
133 | 48, 22, 132 | syl2anc 661 |
. . . . 5
|
134 | 46, 133 | mpbird 232 |
. . . 4
|
135 | 128, 131,
134 | 3eqtr3d 2506 |
. . 3
|
136 | 135 | oveq2d 6312 |
. 2
|
137 | 136, 127 | eqtr3d 2500 |
1
|