Step | Hyp | Ref
| Expression |
1 | | frecuzrdgrclt.c |
. . . . . 6
   |
2 | | frecuzrdgrclt.a |
. . . . . 6
   |
3 | | frecuzrdgrclt.t |
. . . . . 6

  |
4 | | frecuzrdgrclt.f |
. . . . . 6
 
    
        |
5 | | frecuzrdgrclt.r |
. . . . . 6
frec      
                |
6 | | frecuzrdgsuctlem.ran |
. . . . . 6
   |
7 | 1, 2, 3, 4, 5, 6 | frecuzrdgtclt 10407 |
. . . . 5
           |
8 | 7 | adantr 276 |
. . . 4
 
    
          |
9 | | ffun 5364 |
. . . 4
           |
10 | 8, 9 | syl 14 |
. . 3
 
    
  |
11 | | 1st2nd2 6170 |
. . . . . . . . . . . . . . 15
      
             |
12 | 11 | adantl 277 |
. . . . . . . . . . . . . 14
       
      
             |
13 | 12 | fveq2d 5515 |
. . . . . . . . . . . . 13
       
      
                                                     |
14 | | df-ov 5872 |
. . . . . . . . . . . . 13
                                                            |
15 | 13, 14 | eqtr4di 2228 |
. . . . . . . . . . . 12
       
      
                               
                  |
16 | | xp1st 6160 |
. . . . . . . . . . . . . 14
      
          |
17 | 16 | adantl 277 |
. . . . . . . . . . . . 13
       
      
          |
18 | 3 | ad2antrr 488 |
. . . . . . . . . . . . . 14
       
      
  |
19 | | xp2nd 6161 |
. . . . . . . . . . . . . . 15
      
      |
20 | 19 | adantl 277 |
. . . . . . . . . . . . . 14
       
      
      |
21 | 18, 20 | sseldd 3156 |
. . . . . . . . . . . . 13
       
      
      |
22 | | peano2uz 9572 |
. . . . . . . . . . . . . . 15
        
            |
23 | 17, 22 | syl 14 |
. . . . . . . . . . . . . 14
       
      
            |
24 | | oveq2 5877 |
. . . . . . . . . . . . . . . 16
    
                      |
25 | 24 | eleq1d 2246 |
. . . . . . . . . . . . . . 15
    
        
               |
26 | | oveq1 5876 |
. . . . . . . . . . . . . . . . . 18
    
              |
27 | 26 | eleq1d 2246 |
. . . . . . . . . . . . . . . . 17
    
    
           |
28 | 27 | ralbidv 2477 |
. . . . . . . . . . . . . . . 16
    
 
   

           |
29 | 4 | ralrimivva 2559 |
. . . . . . . . . . . . . . . . 17
       
      |
30 | 29 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
       
      
      
      |
31 | 28, 30, 17 | rspcdva 2846 |
. . . . . . . . . . . . . . 15
       
      

          |
32 | 25, 31, 20 | rspcdva 2846 |
. . . . . . . . . . . . . 14
       
      
              |
33 | | opelxpi 4655 |
. . . . . . . . . . . . . 14
           
            
                             |
34 | 23, 32, 33 | syl2anc 411 |
. . . . . . . . . . . . 13
       
      
                             |
35 | | oveq1 5876 |
. . . . . . . . . . . . . . 15
    
          |
36 | 35, 26 | opeq12d 3784 |
. . . . . . . . . . . . . 14
    
        
                   |
37 | 24 | opeq2d 3783 |
. . . . . . . . . . . . . 14
    
                
                       |
38 | | eqid 2177 |
. . . . . . . . . . . . . 14
               
                 |
39 | 36, 37, 38 | ovmpog 6003 |
. . . . . . . . . . . . 13
                                  
                  
                                       |
40 | 17, 21, 34, 39 | syl3anc 1238 |
. . . . . . . . . . . 12
       
      
                                                   |
41 | 15, 40 | eqtrd 2210 |
. . . . . . . . . . 11
       
      
                                           |
42 | 41, 34 | eqeltrd 2254 |
. . . . . . . . . 10
       
      
                            |
43 | 42 | ralrimiva 2550 |
. . . . . . . . 9
 
    
              
                     |
44 | | uzid 9531 |
. . . . . . . . . . . 12
       |
45 | 1, 44 | syl 14 |
. . . . . . . . . . 11
       |
46 | | opelxpi 4655 |
. . . . . . . . . . 11
                  |
47 | 45, 2, 46 | syl2anc 411 |
. . . . . . . . . 10
            |
48 | 47 | adantr 276 |
. . . . . . . . 9
 
    
           |
49 | | frecuzrdgsuctlem.g |
. . . . . . . . . . 11
frec        |
50 | 1, 49 | frec2uzf1od 10392 |
. . . . . . . . . 10
           |
51 | | f1ocnvdm 5776 |
. . . . . . . . . 10
         
            |
52 | 50, 51 | sylan 283 |
. . . . . . . . 9
 
    
       |
53 | | frecsuc 6402 |
. . . . . . . . 9
                                                   frec                                                 frec                                 |
54 | 43, 48, 52, 53 | syl3anc 1238 |
. . . . . . . 8
 
    
frec                                                 frec                                 |
55 | 5 | fveq1i 5512 |
. . . . . . . 8
  
      frec                               |
56 | 5 | fveq1i 5512 |
. . . . . . . . 9
         frec                               |
57 | 56 | fveq2i 5514 |
. . . . . . . 8
                                                frec                                |
58 | 54, 55, 57 | 3eqtr4g 2235 |
. . . . . . 7
 
    
               
                        |
59 | 1, 2, 3, 4, 5 | frecuzrdgrclt 10401 |
. . . . . . . . . . . 12
             |
60 | 59 | adantr 276 |
. . . . . . . . . . 11
 
    
            |
61 | 60, 52 | ffvelcdmd 5648 |
. . . . . . . . . 10
 
    
                 |
62 | | 1st2nd2 6170 |
. . . . . . . . . 10
                                                        |
63 | 61, 62 | syl 14 |
. . . . . . . . 9
 
    
                                        |
64 | 1 | adantr 276 |
. . . . . . . . . . . 12
 
    
  |
65 | 2 | adantr 276 |
. . . . . . . . . . . 12
 
    
  |
66 | 3 | adantr 276 |
. . . . . . . . . . . 12
 
    
  |
67 | 4 | adantlr 477 |
. . . . . . . . . . . 12
       
    
        |
68 | 64, 65, 66, 67, 5, 52, 49 | frecuzrdgg 10402 |
. . . . . . . . . . 11
 
    
                        |
69 | | f1ocnvfv2 5773 |
. . . . . . . . . . . 12
         
                |
70 | 50, 69 | sylan 283 |
. . . . . . . . . . 11
 
    
           |
71 | 68, 70 | eqtrd 2210 |
. . . . . . . . . 10
 
    
               |
72 | 71 | opeq1d 3782 |
. . . . . . . . 9
 
    
                            
                  |
73 | 63, 72 | eqtrd 2210 |
. . . . . . . 8
 
    
                           |
74 | 73 | fveq2d 5515 |
. . . . . . 7
 
    
                                                                   |
75 | 58, 74 | eqtrd 2210 |
. . . . . 6
 
    
               
                               |
76 | | df-ov 5872 |
. . . . . 6
                                       
                              |
77 | 75, 76 | eqtr4di 2228 |
. . . . 5
 
    
                                            |
78 | | simpr 110 |
. . . . . 6
 
    
      |
79 | | xp2nd 6161 |
. . . . . . . 8
                               |
80 | 61, 79 | syl 14 |
. . . . . . 7
 
    
               |
81 | 66, 80 | sseldd 3156 |
. . . . . 6
 
    
               |
82 | | peano2uz 9572 |
. . . . . . . 8
    
        |
83 | 82 | adantl 277 |
. . . . . . 7
 
    
        |
84 | 67, 78, 80 | caovcld 6022 |
. . . . . . 7
 
    
                   |
85 | | opelxp 4653 |
. . . . . . 7
                                                        |
86 | 83, 84, 85 | sylanbrc 417 |
. . . . . 6
 
    
                     
        |
87 | | oveq1 5876 |
. . . . . . . 8
       |
88 | | oveq1 5876 |
. . . . . . . 8
           |
89 | 87, 88 | opeq12d 3784 |
. . . . . . 7
                     |
90 | | oveq2 5877 |
. . . . . . . 8
                                     |
91 | 90 | opeq2d 3783 |
. . . . . . 7
               
                               |
92 | 89, 91, 38 | ovmpog 6003 |
. . . . . 6
                                               
                                                         |
93 | 78, 81, 86, 92 | syl3anc 1238 |
. . . . 5
 
    
                                                         |
94 | 77, 93 | eqtrd 2210 |
. . . 4
 
    
                                 |
95 | | ffun 5364 |
. . . . . . 7
             |
96 | 60, 95 | syl 14 |
. . . . . 6
 
    
  |
97 | | peano2 4591 |
. . . . . . . 8
             |
98 | 52, 97 | syl 14 |
. . . . . . 7
 
    
       |
99 | | fdm 5367 |
. . . . . . . 8
             |
100 | 60, 99 | syl 14 |
. . . . . . 7
 
    
  |
101 | 98, 100 | eleqtrrd 2257 |
. . . . . 6
 
    
       |
102 | | fvelrn 5643 |
. . . . . 6
                   |
103 | 96, 101, 102 | syl2anc 411 |
. . . . 5
 
    
           |
104 | 6 | adantr 276 |
. . . . 5
 
    
  |
105 | 103, 104 | eleqtrrd 2257 |
. . . 4
 
    
           |
106 | 94, 105 | eqeltrrd 2255 |
. . 3
 
    
                     
  |
107 | | funopfv 5551 |
. . 3

                      
                          |
108 | 10, 106, 107 | sylc 62 |
. 2
 
    
                         |
109 | 52, 100 | eleqtrrd 2257 |
. . . . . . 7
 
    
       |
110 | | fvelrn 5643 |
. . . . . . 7
                   |
111 | 96, 109, 110 | syl2anc 411 |
. . . . . 6
 
    
           |
112 | 111, 104 | eleqtrrd 2257 |
. . . . 5
 
    
           |
113 | 73, 112 | eqeltrrd 2255 |
. . . 4
 
    
                  |
114 | | funopfv 5551 |
. . . 4

                                     |
115 | 10, 113, 114 | sylc 62 |
. . 3
 
    
                   |
116 | 115 | oveq2d 5885 |
. 2
 
    
                           |
117 | 108, 116 | eqtr4d 2213 |
1
 
    
                |