Step | Hyp | Ref
| Expression |
1 | | frec2uz.1 |
. . . . . . 7
   |
2 | 1 | adantr 276 |
. . . . . 6
 
    
  |
3 | | frec2uz.2 |
. . . . . 6
frec        |
4 | | frecuzrdgrrn.a |
. . . . . . 7
   |
5 | 4 | adantr 276 |
. . . . . 6
 
    
  |
6 | | frecuzrdgrrn.f |
. . . . . . 7
 
    
        |
7 | 6 | adantlr 477 |
. . . . . 6
       
    
        |
8 | | frecuzrdgrrn.2 |
. . . . . 6
frec      
                |
9 | | peano2uz 9583 |
. . . . . . 7
    
        |
10 | 9 | adantl 277 |
. . . . . 6
 
    
        |
11 | 2, 3, 5, 7, 8, 10 | frecuzrdglem 10411 |
. . . . 5
 
    
                      |
12 | | frecuzrdgtcl.3 |
. . . . . 6
   |
13 | 12 | adantr 276 |
. . . . 5
 
    
  |
14 | 11, 13 | eleqtrrd 2257 |
. . . 4
 
    
                      |
15 | 1, 3, 4, 6, 8, 12 | frecuzrdgtcl 10412 |
. . . . . . 7
           |
16 | | ffun 5369 |
. . . . . . 7
           |
17 | 15, 16 | syl 14 |
. . . . . 6
   |
18 | | funopfv 5556 |
. . . . . 6

                        
                    |
19 | 17, 18 | syl 14 |
. . . . 5
                                              |
20 | 19 | adantr 276 |
. . . 4
 
    
                        
                    |
21 | 14, 20 | mpd 13 |
. . 3
 
    
                       |
22 | 1, 3 | frec2uzf1od 10406 |
. . . . . . . . 9
           |
23 | | f1ocnvdm 5782 |
. . . . . . . . 9
         
            |
24 | 22, 23 | sylan 283 |
. . . . . . . 8
 
    
       |
25 | 2, 3, 24 | frec2uzsucd 10401 |
. . . . . . 7
 
    
                      |
26 | | f1ocnvfv2 5779 |
. . . . . . . . 9
         
                |
27 | 22, 26 | sylan 283 |
. . . . . . . 8
 
    
           |
28 | 27 | oveq1d 5890 |
. . . . . . 7
 
    
               |
29 | 25, 28 | eqtrd 2210 |
. . . . . 6
 
    
             |
30 | | peano2 4595 |
. . . . . . . 8
             |
31 | 24, 30 | syl 14 |
. . . . . . 7
 
    
       |
32 | | f1ocnvfv 5780 |
. . . . . . 7
                   
            
          |
33 | 22, 31, 32 | syl2an2r 595 |
. . . . . 6
 
    
                
          |
34 | 29, 33 | mpd 13 |
. . . . 5
 
    
              |
35 | 34 | fveq2d 5520 |
. . . 4
 
    
       
              |
36 | 35 | fveq2d 5520 |
. . 3
 
    
                    
         |
37 | 21, 36 | eqtrd 2210 |
. 2
 
    
           
         |
38 | | 1st2nd2 6176 |
. . . . . . . . . . 11
      
             |
39 | 38 | adantl 277 |
. . . . . . . . . 10
       
      
             |
40 | 39 | fveq2d 5520 |
. . . . . . . . 9
       
      
                                                     |
41 | | df-ov 5878 |
. . . . . . . . . . 11
                                                            |
42 | | xp1st 6166 |
. . . . . . . . . . . . 13
      
          |
43 | 42 | adantl 277 |
. . . . . . . . . . . 12
       
      
          |
44 | | xp2nd 6167 |
. . . . . . . . . . . . 13
      
      |
45 | 44 | adantl 277 |
. . . . . . . . . . . 12
       
      
      |
46 | | peano2uz 9583 |
. . . . . . . . . . . . . 14
        
            |
47 | 43, 46 | syl 14 |
. . . . . . . . . . . . 13
       
      
            |
48 | | oveq2 5883 |
. . . . . . . . . . . . . . 15
    
                      |
49 | 48 | eleq1d 2246 |
. . . . . . . . . . . . . 14
    
        
               |
50 | | oveq1 5882 |
. . . . . . . . . . . . . . . . 17
    
              |
51 | 50 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
    
    
           |
52 | 51 | ralbidv 2477 |
. . . . . . . . . . . . . . 15
    
 
   

           |
53 | 6 | ralrimivva 2559 |
. . . . . . . . . . . . . . . 16
       
      |
54 | 53 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
       
      
      
      |
55 | 52, 54, 43 | rspcdva 2847 |
. . . . . . . . . . . . . 14
       
      

          |
56 | 49, 55, 45 | rspcdva 2847 |
. . . . . . . . . . . . 13
       
      
              |
57 | | opelxp 4657 |
. . . . . . . . . . . . 13
                     
     
          
               |
58 | 47, 56, 57 | sylanbrc 417 |
. . . . . . . . . . . 12
       
      
                             |
59 | | oveq1 5882 |
. . . . . . . . . . . . . 14
    
          |
60 | 59, 50 | opeq12d 3787 |
. . . . . . . . . . . . 13
    
        
                   |
61 | 48 | opeq2d 3786 |
. . . . . . . . . . . . 13
    
                
                       |
62 | | eqid 2177 |
. . . . . . . . . . . . 13
               
                 |
63 | 60, 61, 62 | ovmpog 6009 |
. . . . . . . . . . . 12
                                  
                  
                                       |
64 | 43, 45, 58, 63 | syl3anc 1238 |
. . . . . . . . . . 11
       
      
                                                   |
65 | 41, 64 | eqtr3id 2224 |
. . . . . . . . . 10
       
      
                                                      |
66 | 65, 58 | eqeltrd 2254 |
. . . . . . . . 9
       
      
                                       |
67 | 40, 66 | eqeltrd 2254 |
. . . . . . . 8
       
      
                            |
68 | 67 | ralrimiva 2550 |
. . . . . . 7
 
    
              
                     |
69 | | uzid 9542 |
. . . . . . . . 9
       |
70 | 2, 69 | syl 14 |
. . . . . . . 8
 
    
      |
71 | | opelxp 4657 |
. . . . . . . 8
  
           
   |
72 | 70, 5, 71 | sylanbrc 417 |
. . . . . . 7
 
    
           |
73 | | frecsuc 6408 |
. . . . . . 7
                                                   frec                                                 frec                                 |
74 | 68, 72, 24, 73 | syl3anc 1238 |
. . . . . 6
 
    
frec                                                 frec                                 |
75 | 8 | fveq1i 5517 |
. . . . . 6
  
      frec                               |
76 | 8 | fveq1i 5517 |
. . . . . . 7
         frec                               |
77 | 76 | fveq2i 5519 |
. . . . . 6
                                                frec                                |
78 | 74, 75, 77 | 3eqtr4g 2235 |
. . . . 5
 
    
               
                        |
79 | 2, 3, 5, 7, 8, 24 | frec2uzrdg 10409 |
. . . . . . 7
 
    
                                    |
80 | 79 | fveq2d 5520 |
. . . . . 6
 
    
                                                                            |
81 | | df-ov 5878 |
. . . . . 6
                
                               
                                       |
82 | 80, 81 | eqtr4di 2228 |
. . . . 5
 
    
                                             
                           |
83 | 2, 3, 24 | frec2uzuzd 10402 |
. . . . . 6
 
    
               |
84 | 2, 3, 5, 7, 8 | frecuzrdgrrn 10408 |
. . . . . . . 8
       
                       |
85 | 24, 84 | mpdan 421 |
. . . . . . 7
 
    
                 |
86 | | xp2nd 6167 |
. . . . . . 7
                               |
87 | 85, 86 | syl 14 |
. . . . . 6
 
    
               |
88 | 28, 10 | eqeltrd 2254 |
. . . . . . 7
 
    
                 |
89 | 7 | caovclg 6027 |
. . . . . . . 8
       
    
        |
90 | 89, 83, 87 | caovcld 6028 |
. . . . . . 7
 
    
                            |
91 | | opelxp 4657 |
. . . . . . 7
                                                                                            |
92 | 88, 90, 91 | sylanbrc 417 |
. . . . . 6
 
    
                                                |
93 | | oveq1 5882 |
. . . . . . . 8
         
               |
94 | | oveq1 5882 |
. . . . . . . 8
         
                   |
95 | 93, 94 | opeq12d 3787 |
. . . . . . 7
         
        
                             |
96 | | oveq2 5883 |
. . . . . . . 8
                                                       |
97 | 96 | opeq2d 3786 |
. . . . . . 7
                                                                                   |
98 | | oveq1 5882 |
. . . . . . . . 9
       |
99 | | oveq1 5882 |
. . . . . . . . 9
           |
100 | 98, 99 | opeq12d 3787 |
. . . . . . . 8
                     |
101 | | oveq2 5883 |
. . . . . . . . 9
           |
102 | 101 | opeq2d 3786 |
. . . . . . . 8
                     |
103 | 100, 102 | cbvmpov 5955 |
. . . . . . 7
               
     
           |
104 | 95, 97, 103 | ovmpog 6009 |
. . . . . 6
                                                                          
                
                                                                   |
105 | 83, 87, 92, 104 | syl3anc 1238 |
. . . . 5
 
    
                
                                                                   |
106 | 78, 82, 105 | 3eqtrd 2214 |
. . . 4
 
    
                                                   |
107 | 106 | fveq2d 5520 |
. . 3
 
    
                                                           |
108 | | op2ndg 6152 |
. . . 4
                
                                                                                                   |
109 | 88, 90, 108 | syl2anc 411 |
. . 3
 
    
                                                                        |
110 | 107, 109 | eqtrd 2210 |
. 2
 
    
                                         |
111 | | simpr 110 |
. . . . . . 7
 
    
      |
112 | 2, 3, 5, 7, 8, 111 | frecuzrdglem 10411 |
. . . . . 6
 
    
                  |
113 | 112, 13 | eleqtrrd 2257 |
. . . . 5
 
    
                  |
114 | | funopfv 5556 |
. . . . . . 7

                                     |
115 | 17, 114 | syl 14 |
. . . . . 6
                                      |
116 | 115 | adantr 276 |
. . . . 5
 
    
                                     |
117 | 113, 116 | mpd 13 |
. . . 4
 
    
                   |
118 | 117 | eqcomd 2183 |
. . 3
 
    
                   |
119 | 27, 118 | oveq12d 5893 |
. 2
 
    
                                    |
120 | 37, 110, 119 | 3eqtrd 2214 |
1
 
    
                |