Step | Hyp | Ref
| Expression |
1 | | fucpropd.1 |
. . . . 5
 
f   
f     |
2 | | fucpropd.2 |
. . . . 5
 compf  compf    |
3 | | fucpropd.3 |
. . . . 5
 
f   
f     |
4 | | fucpropd.4 |
. . . . 5
 compf  compf    |
5 | | fucpropd.a |
. . . . 5
   |
6 | | fucpropd.b |
. . . . 5
   |
7 | | fucpropd.c |
. . . . 5
   |
8 | | fucpropd.d |
. . . . 5
   |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | funcpropd 15816 |
. . . 4
       |
10 | 9 | opeq2d 4143 |
. . 3
      
              |
11 | 1, 2, 3, 4, 5, 6, 7, 8 | natpropd 15892 |
. . . 4
  Nat   Nat    |
12 | 11 | opeq2d 4143 |
. . 3
     
 Nat  
      Nat     |
13 | 9 | sqxpeqd 4838 |
. . . . 5
               |
14 | 9 | adantr 471 |
. . . . 5
 
             |
15 | | nfv 1765 |
. . . . . 6
     
         |
16 | | nfcsb1v 3347 |
. . . . . . 7
        ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                     |
17 | 16 | a1i 11 |
. . . . . 6
 
      
            ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
18 | | fvex 5858 |
. . . . . . 7
     |
19 | 18 | a1i 11 |
. . . . . 6
 
      
          |
20 | | nfv 1765 |
. . . . . . . 8
          
          |
21 | | nfcsb1v 3347 |
. . . . . . . . 9
        ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                     |
22 | 21 | a1i 11 |
. . . . . . . 8
     
       
             ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
23 | | fvex 5858 |
. . . . . . . . 9
     |
24 | 23 | a1i 11 |
. . . . . . . 8
     
       
           |
25 | 11 | ad3antrrr 741 |
. . . . . . . . . . 11
          
               Nat   Nat    |
26 | 25 | oveqd 6293 |
. . . . . . . . . 10
          
                 Nat       Nat      |
27 | 25 | oveqdr 6300 |
. . . . . . . . . 10
           
                 Nat    
   Nat       Nat      |
28 | 1 | homfeqbas 15612 |
. . . . . . . . . . . 12
           |
29 | 28 | ad4antr 743 |
. . . . . . . . . . 11
           
                  Nat       Nat                |
30 | | eqid 2452 |
. . . . . . . . . . . 12
         |
31 | | eqid 2452 |
. . . . . . . . . . . 12
       |
32 | | eqid 2452 |
. . . . . . . . . . . 12
comp  comp   |
33 | | eqid 2452 |
. . . . . . . . . . . 12
comp  comp   |
34 | 3 | ad5antr 745 |
. . . . . . . . . . . 12
     
      
                  Nat       Nat            f    f     |
35 | 4 | ad5antr 745 |
. . . . . . . . . . . 12
     
      
                  Nat       Nat           compf  compf    |
36 | | eqid 2452 |
. . . . . . . . . . . . . 14
         |
37 | | relfunc 15778 |
. . . . . . . . . . . . . . 15
   |
38 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
           
                  Nat       Nat            |
39 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . 18
           
                  Nat       Nat        
         |
40 | 39 | simpld 465 |
. . . . . . . . . . . . . . . . 17
           
                  Nat       Nat              |
41 | | xp1st 6811 |
. . . . . . . . . . . . . . . . 17
               |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
           
                  Nat       Nat              |
43 | 38, 42 | eqeltrd 2530 |
. . . . . . . . . . . . . . 15
           
                  Nat       Nat          |
44 | | 1st2ndbr 6830 |
. . . . . . . . . . . . . . 15
            
        |
45 | 37, 43, 44 | sylancr 674 |
. . . . . . . . . . . . . 14
           
                  Nat       Nat           
        |
46 | 36, 30, 45 | funcf1 15782 |
. . . . . . . . . . . . 13
           
                  Nat       Nat                        |
47 | 46 | ffvelrnda 6006 |
. . . . . . . . . . . 12
     
      
                  Nat       Nat                         |
48 | | simplr 767 |
. . . . . . . . . . . . . . . 16
           
                  Nat       Nat            |
49 | | xp2nd 6812 |
. . . . . . . . . . . . . . . . 17
               |
50 | 40, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
           
                  Nat       Nat              |
51 | 48, 50 | eqeltrd 2530 |
. . . . . . . . . . . . . . 15
           
                  Nat       Nat          |
52 | | 1st2ndbr 6830 |
. . . . . . . . . . . . . . 15
            
        |
53 | 37, 51, 52 | sylancr 674 |
. . . . . . . . . . . . . 14
           
                  Nat       Nat           
        |
54 | 36, 30, 53 | funcf1 15782 |
. . . . . . . . . . . . 13
           
                  Nat       Nat                        |
55 | 54 | ffvelrnda 6006 |
. . . . . . . . . . . 12
     
      
                  Nat       Nat                         |
56 | 39 | simprd 469 |
. . . . . . . . . . . . . . 15
           
                  Nat       Nat          |
57 | | 1st2ndbr 6830 |
. . . . . . . . . . . . . . 15
            
        |
58 | 37, 56, 57 | sylancr 674 |
. . . . . . . . . . . . . 14
           
                  Nat       Nat           
        |
59 | 36, 30, 58 | funcf1 15782 |
. . . . . . . . . . . . 13
           
                  Nat       Nat                        |
60 | 59 | ffvelrnda 6006 |
. . . . . . . . . . . 12
     
      
                  Nat       Nat                         |
61 | | eqid 2452 |
. . . . . . . . . . . . 13
 Nat   Nat   |
62 | | simplrr 776 |
. . . . . . . . . . . . . 14
     
      
                  Nat       Nat              Nat      |
63 | 61, 62 | nat1st2nd 15867 |
. . . . . . . . . . . . 13
     
      
                  Nat       Nat                         Nat                 |
64 | | simpr 467 |
. . . . . . . . . . . . 13
     
      
                  Nat       Nat                 |
65 | 61, 63, 36, 31, 64 | natcl 15869 |
. . . . . . . . . . . 12
     
      
                  Nat       Nat                                        |
66 | | simplrl 775 |
. . . . . . . . . . . . . 14
     
      
                  Nat       Nat              Nat      |
67 | 61, 66 | nat1st2nd 15867 |
. . . . . . . . . . . . 13
     
      
                  Nat       Nat                         Nat                 |
68 | 61, 67, 36, 31, 64 | natcl 15869 |
. . . . . . . . . . . 12
     
      
                  Nat       Nat                                        |
69 | 30, 31, 32, 33, 34, 35, 47, 55, 60, 65, 68 | comfeqval 15624 |
. . . . . . . . . . 11
     
      
                  Nat       Nat                                      comp                                             comp                    |
70 | 29, 69 | mpteq12dva 4452 |
. . . . . . . . . 10
           
                  Nat       Nat                                      comp                                                   comp                     |
71 | 26, 27, 70 | mpt2eq123dva 6340 |
. . . . . . . . 9
          
                  Nat        Nat                                    comp                        Nat        Nat                                    comp                      |
72 | | csbeq1a 3340 |
. . . . . . . . . 10
    
    Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
73 | 72 | adantl 472 |
. . . . . . . . 9
          
                  Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
74 | 71, 73 | eqtrd 2486 |
. . . . . . . 8
          
                  Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
75 | 20, 22, 24, 74 | csbiedf 3352 |
. . . . . . 7
     
       
           ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
76 | | csbeq1a 3340 |
. . . . . . . 8
    
      ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
77 | 76 | adantl 472 |
. . . . . . 7
     
       
           ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
78 | 75, 77 | eqtrd 2486 |
. . . . . 6
     
       
           ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
79 | 15, 17, 19, 78 | csbiedf 3352 |
. . . . 5
 
      
          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                          ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
80 | 13, 14, 79 | mpt2eq123dva 6340 |
. . . 4
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                       |
81 | 80 | opeq2d 4143 |
. . 3
  comp                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                       comp  
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                        |
82 | 10, 12, 81 | tpeq123d 4035 |
. 2
       
          Nat   
 comp           
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      
                 Nat   
 comp           
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         |
83 | | eqid 2452 |
. . 3
 FuncCat   FuncCat   |
84 | | eqid 2452 |
. . 3
  
  |
85 | | eqidd 2453 |
. . 3
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                       |
86 | 83, 84, 61, 36, 32, 5, 7, 85 | fucval 15874 |
. 2
  FuncCat
       
          Nat   
 comp           
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         |
87 | | eqid 2452 |
. . 3
 FuncCat   FuncCat   |
88 | | eqid 2452 |
. . 3
  
  |
89 | | eqid 2452 |
. . 3
 Nat   Nat   |
90 | | eqid 2452 |
. . 3
         |
91 | | eqidd 2453 |
. . 3
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                       |
92 | 87, 88, 89, 90, 33, 6, 8, 91 | fucval 15874 |
. 2
  FuncCat
       
          Nat   
 comp           
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         |
93 | 82, 86, 92 | 3eqtr4d 2496 |
1
  FuncCat
  FuncCat    |