Step | Hyp | Ref
| Expression |
1 | | elfznn 11828 |
. . . . . . . 8
                 
  |
2 | 1 | a1i 11 |
. . . . . . 7
 
        
                 
   |
3 | | cnvimass 5188 |
. . . . . . . . 9
        
 |
4 | | isercoll.g |
. . . . . . . . . . 11
       |
5 | 4 | adantr 467 |
. . . . . . . . . 10
 
        
      |
6 | | fdm 5733 |
. . . . . . . . . 10
       |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
 
        
  |
8 | 3, 7 | syl5sseq 3480 |
. . . . . . . 8
 
        
           |
9 | 8 | sseld 3431 |
. . . . . . 7
 
        
             |
10 | | id 22 |
. . . . . . . . . . 11
   |
11 | | nnuz 11194 |
. . . . . . . . . . 11
     |
12 | 10, 11 | syl6eleq 2539 |
. . . . . . . . . 10
       |
13 | | ltso 9714 |
. . . . . . . . . . . . . 14
 |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
 
        
  |
15 | | fzfid 12186 |
. . . . . . . . . . . . . . 15
 
        
      |
16 | | ffun 5731 |
. . . . . . . . . . . . . . . . 17
       |
17 | | funimacnv 5655 |
. . . . . . . . . . . . . . . . 17

                     |
18 | 5, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . 16
 
        
                     |
19 | | inss1 3652 |
. . . . . . . . . . . . . . . 16
    
      |
20 | 18, 19 | syl6eqss 3482 |
. . . . . . . . . . . . . . 15
 
        
                   |
21 | | ssfi 7792 |
. . . . . . . . . . . . . . 15
                  
                    |
22 | 15, 20, 21 | syl2anc 667 |
. . . . . . . . . . . . . 14
 
        
               |
23 | | ssid 3451 |
. . . . . . . . . . . . . . . . . . . . 21
 |
24 | | isercoll.z |
. . . . . . . . . . . . . . . . . . . . . 22
     |
25 | | isercoll.m |
. . . . . . . . . . . . . . . . . . . . . 22
   |
26 | | isercoll.i |
. . . . . . . . . . . . . . . . . . . . . 22
 

            |
27 | 24, 25, 4, 26 | isercolllem1 13728 |
. . . . . . . . . . . . . . . . . . . . 21
 
  
         |
28 | 23, 27 | mpan2 677 |
. . . . . . . . . . . . . . . . . . . 20
    
       |
29 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
30 | | fnresdm 5685 |
. . . . . . . . . . . . . . . . . . . . 21
     |
31 | | isoeq1 6210 |
. . . . . . . . . . . . . . . . . . . . 21
 

 
  
    
          |
32 | 4, 29, 30, 31 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . 20
   
      
          |
33 | 28, 32 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19

         |
34 | | isof1o 6216 |
. . . . . . . . . . . . . . . . . . 19
  
               |
35 | | f1ocnv 5826 |
. . . . . . . . . . . . . . . . . . 19
                    |
36 | | f1ofun 5816 |
. . . . . . . . . . . . . . . . . . 19
             |
37 | 33, 34, 35, 36 | 4syl 19 |
. . . . . . . . . . . . . . . . . 18
    |
38 | | df-f1 5587 |
. . . . . . . . . . . . . . . . . 18
    
         |
39 | 4, 37, 38 | sylanbrc 670 |
. . . . . . . . . . . . . . . . 17
       |
40 | 39 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
        
      |
41 | | nnex 10615 |
. . . . . . . . . . . . . . . . 17
 |
42 | | ssexg 4549 |
. . . . . . . . . . . . . . . . 17
                       |
43 | 8, 41, 42 | sylancl 668 |
. . . . . . . . . . . . . . . 16
 
        
           |
44 | | f1imaeng 7629 |
. . . . . . . . . . . . . . . 16
                                                 |
45 | 40, 8, 43, 44 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
 
        
                        |
46 | 45 | ensymd 7620 |
. . . . . . . . . . . . . 14
 
        
                        |
47 | | enfii 7789 |
. . . . . . . . . . . . . 14
                                                 |
48 | 22, 46, 47 | syl2anc 667 |
. . . . . . . . . . . . 13
 
        
           |
49 | | 1nn 10620 |
. . . . . . . . . . . . . . . 16
 |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
 
        
  |
51 | | ffvelrn 6020 |
. . . . . . . . . . . . . . . . . . 19
     
       |
52 | 4, 49, 51 | sylancl 668 |
. . . . . . . . . . . . . . . . . 18
       |
53 | 52, 24 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . 17
           |
54 | 53 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
        
          |
55 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
        
          |
56 | | elfzuzb 11794 |
. . . . . . . . . . . . . . . 16
        
        
           |
57 | 54, 55, 56 | sylanbrc 670 |
. . . . . . . . . . . . . . 15
 
        
          |
58 | 5, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
 
        
  |
59 | | elpreima 6002 |
. . . . . . . . . . . . . . . 16
                        |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . 15
 
        
         
             |
61 | 50, 57, 60 | mpbir2and 933 |
. . . . . . . . . . . . . 14
 
        
           |
62 | | ne0i 3737 |
. . . . . . . . . . . . . 14
                     |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . 13
 
        
           |
64 | | nnssre 10613 |
. . . . . . . . . . . . . 14
 |
65 | 8, 64 | syl6ss 3444 |
. . . . . . . . . . . . 13
 
        
           |
66 | | fisupcl 7985 |
. . . . . . . . . . . . 13
                                                       |
67 | 14, 48, 63, 65, 66 | syl13anc 1270 |
. . . . . . . . . . . 12
 
        
                        |
68 | 8, 67 | sseldd 3433 |
. . . . . . . . . . 11
 
        
               |
69 | 68 | nnzd 11039 |
. . . . . . . . . 10
 
        
               |
70 | | elfz5 11792 |
. . . . . . . . . 10
                                     
                |
71 | 12, 69, 70 | syl2anr 481 |
. . . . . . . . 9
                              
                |
72 | | elpreima 6002 |
. . . . . . . . . . . . . . . . . 18
                                                               |
73 | 58, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
        
                                                              |
74 | 67, 73 | mpbid 214 |
. . . . . . . . . . . . . . . 16
 
        
                                      |
75 | 74 | simprd 465 |
. . . . . . . . . . . . . . 15
 
        
                       |
76 | | elfzle2 11803 |
. . . . . . . . . . . . . . 15
                     
                
  |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . 14
 
        
                
  |
78 | 77 | adantr 467 |
. . . . . . . . . . . . 13
                             
  |
79 | | uzssz 11178 |
. . . . . . . . . . . . . . . . 17
     |
80 | 24, 79 | eqsstri 3462 |
. . . . . . . . . . . . . . . 16
 |
81 | | zssre 10944 |
. . . . . . . . . . . . . . . 16
 |
82 | 80, 81 | sstri 3441 |
. . . . . . . . . . . . . . 15
 |
83 | 5 | ffvelrnda 6022 |
. . . . . . . . . . . . . . 15
                   |
84 | 82, 83 | sseldi 3430 |
. . . . . . . . . . . . . 14
                   |
85 | 5, 68 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 
        
                   |
86 | 85 | adantr 467 |
. . . . . . . . . . . . . . 15
                                |
87 | 82, 86 | sseldi 3430 |
. . . . . . . . . . . . . 14
                                |
88 | | eluzelz 11168 |
. . . . . . . . . . . . . . . 16
        
  |
89 | 88 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
               |
90 | 81, 89 | sseldi 3430 |
. . . . . . . . . . . . . 14
               |
91 | | letr 9727 |
. . . . . . . . . . . . . 14
                                                               
    
   |
92 | 84, 87, 90, 91 | syl3anc 1268 |
. . . . . . . . . . . . 13
                                                    
    
   |
93 | 78, 92 | mpan2d 680 |
. . . . . . . . . . . 12
                 
                
       |
94 | 33 | ad2antrr 732 |
. . . . . . . . . . . . 13
              
       |
95 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
               |
96 | | ressxr 9684 |
. . . . . . . . . . . . . 14
 |
97 | 95, 96 | syl6ss 3444 |
. . . . . . . . . . . . 13
               |
98 | | imassrn 5179 |
. . . . . . . . . . . . . . . 16
     |
99 | 4 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
                   |
100 | | frn 5735 |
. . . . . . . . . . . . . . . . 17
    
  |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
102 | 98, 101 | syl5ss 3443 |
. . . . . . . . . . . . . . 15
                   |
103 | 102, 82 | syl6ss 3444 |
. . . . . . . . . . . . . 14
                   |
104 | 103, 96 | syl6ss 3444 |
. . . . . . . . . . . . 13
                   |
105 | | simpr 463 |
. . . . . . . . . . . . 13
               |
106 | 68 | adantr 467 |
. . . . . . . . . . . . 13
                            |
107 | | leisorel 12623 |
. . . . . . . . . . . . 13
 
           
                              
                        |
108 | 94, 97, 104, 105, 106, 107 | syl122anc 1277 |
. . . . . . . . . . . 12
             
            
                        |
109 | 83, 24 | syl6eleq 2539 |
. . . . . . . . . . . . 13
                       |
110 | | elfz5 11792 |
. . . . . . . . . . . . 13
                   
       |
111 | 109, 89, 110 | syl2anc 667 |
. . . . . . . . . . . 12
                     
       |
112 | 93, 108, 111 | 3imtr4d 272 |
. . . . . . . . . . 11
             
                        |
113 | | elpreima 6002 |
. . . . . . . . . . . . 13
                        |
114 | 113 | baibd 920 |
. . . . . . . . . . . 12
 
                      |
115 | 58, 114 | sylan 474 |
. . . . . . . . . . 11
                                  |
116 | 112, 115 | sylibrd 238 |
. . . . . . . . . 10
             
                         |
117 | | fimaxre2 10552 |
. . . . . . . . . . . . 13
                                
  |
118 | 65, 48, 117 | syl2anc 667 |
. . . . . . . . . . . 12
 
        
              |
119 | | suprub 10570 |
. . . . . . . . . . . . 13
                     
                                     |
120 | 119 | ex 436 |
. . . . . . . . . . . 12
                    
                                      |
121 | 65, 63, 118, 120 | syl3anc 1268 |
. . . . . . . . . . 11
 
        
                          |
122 | 121 | adantr 467 |
. . . . . . . . . 10
                                       |
123 | 116, 122 | impbid 194 |
. . . . . . . . 9
             
            
            |
124 | 71, 123 | bitrd 257 |
. . . . . . . 8
                              
            |
125 | 124 | ex 436 |
. . . . . . 7
 
        

                 
             |
126 | 2, 9, 125 | pm5.21ndd 356 |
. . . . . 6
 
        
                 
            |
127 | 126 | eqrdv 2449 |
. . . . 5
 
        
                            |
128 | 127 | fveq2d 5869 |
. . . 4
 
        
                                    |
129 | 68 | nnnn0d 10925 |
. . . . 5
 
        
               |
130 | | hashfz1 12529 |
. . . . 5
                                                  |
131 | 129, 130 | syl 17 |
. . . 4
 
        
                                    |
132 | | hashen 12530 |
. . . . . 6
                                                       
                         |
133 | 48, 22, 132 | syl2anc 667 |
. . . . 5
 
        
                                                        |
134 | 46, 133 | mpbird 236 |
. . . 4
 
        
                                |
135 | 128, 131,
134 | 3eqtr3d 2493 |
. . 3
 
        
                                |
136 | 135 | oveq2d 6306 |
. 2
 
        
                                        |
137 | 136, 127 | eqtr3d 2487 |
1
 
        
                                |