Step | Hyp | Ref
| Expression |
1 | | catcfuccl.o |
. . . . 5
 FuncCat
  |
2 | | eqid 2622 |
. . . . 5
  
  |
3 | | eqid 2622 |
. . . . 5
 Nat   Nat   |
4 | | eqid 2622 |
. . . . 5
         |
5 | | eqid 2622 |
. . . . 5
comp  comp   |
6 | | inss2 3834 |
. . . . . 6
   |
7 | | catcfuccl.x |
. . . . . . 7
   |
8 | | catcfuccl.c |
. . . . . . . 8
CatCat   |
9 | | catcfuccl.b |
. . . . . . . 8
     |
10 | | catcfuccl.u |
. . . . . . . 8
 WUni |
11 | 8, 9, 10 | catcbas 16747 |
. . . . . . 7
     |
12 | 7, 11 | eleqtrd 2703 |
. . . . . 6
     |
13 | 6, 12 | sseldi 3601 |
. . . . 5
   |
14 | | catcfuccl.y |
. . . . . . 7
   |
15 | 14, 11 | eleqtrd 2703 |
. . . . . 6
     |
16 | 6, 15 | sseldi 3601 |
. . . . 5
   |
17 | | eqidd 2623 |
. . . . 5
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                       |
18 | 1, 2, 3, 4, 5, 13,
16, 17 | fucval 16618 |
. . . 4
                  Nat   
 comp           
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         |
19 | | df-base 15863 |
. . . . . . 7
Slot  |
20 | | catcfuccl.1 |
. . . . . . . 8
   |
21 | 10, 20 | wunndx 15878 |
. . . . . . 7
   |
22 | 19, 10, 21 | wunstr 15881 |
. . . . . 6
    
  |
23 | | inss1 3833 |
. . . . . . . 8
   |
24 | 23, 12 | sseldi 3601 |
. . . . . . 7
   |
25 | 23, 15 | sseldi 3601 |
. . . . . . 7
   |
26 | 10, 24, 25 | wunfunc 16559 |
. . . . . 6
     |
27 | 10, 22, 26 | wunop 9544 |
. . . . 5
      
     |
28 | | df-hom 15966 |
. . . . . . 7
Slot ;  |
29 | 28, 10, 21 | wunstr 15881 |
. . . . . 6
   
  |
30 | 10, 24, 25 | wunnat 16616 |
. . . . . 6
  Nat    |
31 | 10, 29, 30 | wunop 9544 |
. . . . 5
     
 Nat  
  |
32 | | df-cco 15967 |
. . . . . . 7
comp Slot ;  |
33 | 32, 10, 21 | wunstr 15881 |
. . . . . 6
 comp    |
34 | 10, 26, 26 | wunxp 9546 |
. . . . . . . 8
         |
35 | 10, 34, 26 | wunxp 9546 |
. . . . . . 7
             |
36 | 32, 10, 25 | wunstr 15881 |
. . . . . . . . . . . . . 14
 comp    |
37 | 10, 36 | wunrn 9551 |
. . . . . . . . . . . . 13
 comp    |
38 | 10, 37 | wununi 9528 |
. . . . . . . . . . . 12
  comp    |
39 | 10, 38 | wunrn 9551 |
. . . . . . . . . . 11
  comp    |
40 | 10, 39 | wununi 9528 |
. . . . . . . . . 10
   comp    |
41 | 10, 40 | wunpw 9529 |
. . . . . . . . 9
    comp    |
42 | 19, 10, 24 | wunstr 15881 |
. . . . . . . . 9
       |
43 | 10, 41, 42 | wunmap 9548 |
. . . . . . . 8
     comp         |
44 | 10, 30 | wunrn 9551 |
. . . . . . . . . 10
  Nat    |
45 | 10, 44 | wununi 9528 |
. . . . . . . . 9
   Nat    |
46 | 10, 45, 45 | wunxp 9546 |
. . . . . . . 8
    Nat    Nat     |
47 | 10, 43, 46 | wunpm 9547 |
. . . . . . 7
      comp         
Nat    Nat      |
48 | | fvex 6201 |
. . . . . . . . . . 11
     |
49 | | fvex 6201 |
. . . . . . . . . . . . . 14
     |
50 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
  
 comp        |
51 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . 20
 Nat   |
52 | 51 | rnex 7100 |
. . . . . . . . . . . . . . . . . . 19
 Nat   |
53 | 52 | uniex 6953 |
. . . . . . . . . . . . . . . . . 18
 
Nat   |
54 | 53, 53 | xpex 6962 |
. . . . . . . . . . . . . . . . 17
   Nat    Nat    |
55 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
                                comp                                                   comp                    |
56 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           comp                                        comp             |
57 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     comp             comp   |
58 | | rnss 5354 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      comp             comp                       comp           
 comp    |
59 | | uniss 4458 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                      comp           
 comp                        comp              comp    |
60 | 57, 58, 59 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                      comp           
  comp   |
61 | 56, 60 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           comp                    comp   |
62 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           comp                   |
63 | 62 | elpw 4164 |
. . . . . . . . . . . . . . . . . . . . . . 23
                            comp                     comp                             comp                    comp    |
64 | 61, 63 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . 22
                           comp                     comp   |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
    
                           comp                     comp    |
66 | 55, 65 | fmpti 6383 |
. . . . . . . . . . . . . . . . . . . 20
                                comp                              comp   |
67 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
comp   |
68 | 67 | rnex 7100 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
comp   |
69 | 68 | uniex 6953 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 comp   |
70 | 69 | rnex 7100 |
. . . . . . . . . . . . . . . . . . . . . . 23
 comp   |
71 | 70 | uniex 6953 |
. . . . . . . . . . . . . . . . . . . . . 22
  comp   |
72 | 71 | pwex 4848 |
. . . . . . . . . . . . . . . . . . . . 21
   comp   |
73 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
     |
74 | 72, 73 | elmap 7886 |
. . . . . . . . . . . . . . . . . . . 20
                                 comp                       comp                                       comp                              comp    |
75 | 66, 74 | mpbir 221 |
. . . . . . . . . . . . . . . . . . 19
                                comp                     
 comp        |
76 | 75 | rgen2w 2925 |
. . . . . . . . . . . . . . . . . 18
    Nat         Nat                                     comp                       comp        |
77 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
    Nat        Nat                                    comp                        Nat        Nat                                    comp                     |
78 | 77 | fmpt2 7237 |
. . . . . . . . . . . . . . . . . 18
 
   Nat         Nat                                     comp                     
 comp           Nat        Nat                                    comp                          Nat       Nat         
 comp         |
79 | 76, 78 | mpbi 220 |
. . . . . . . . . . . . . . . . 17
    Nat        Nat                                    comp                          Nat       Nat         
 comp        |
80 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . 18
   Nat     
Nat   |
81 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . 18
   Nat     
Nat   |
82 | | xpss12 5225 |
. . . . . . . . . . . . . . . . . 18
     Nat      Nat     Nat      Nat       Nat       Nat        Nat   
Nat     |
83 | 80, 81, 82 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
    Nat       Nat    
   Nat    Nat    |
84 | | elpm2r 7875 |
. . . . . . . . . . . . . . . . 17
       comp          Nat   
Nat         Nat        Nat                                    comp                          Nat       Nat           comp           Nat       Nat       
Nat    Nat    
    Nat        Nat                                    comp                         comp          Nat   
Nat      |
85 | 50, 54, 79, 83, 84 | mp4an 709 |
. . . . . . . . . . . . . . . 16
    Nat        Nat                                    comp                         comp          Nat   
Nat     |
86 | 85 | sbcth 3450 |
. . . . . . . . . . . . . . 15
           ![]. ].](_drbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat      |
87 | | sbcel1g 3987 |
. . . . . . . . . . . . . . 15
            ![]. ].](_drbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat   
      ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat       |
88 | 86, 87 | mpbid 222 |
. . . . . . . . . . . . . 14
           ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat      |
89 | 49, 88 | ax-mp 5 |
. . . . . . . . . . . . 13
      ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat     |
90 | 89 | sbcth 3450 |
. . . . . . . . . . . 12
           ![]. ].](_drbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat      |
91 | | sbcel1g 3987 |
. . . . . . . . . . . 12
            ![]. ].](_drbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat   
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat       |
92 | 90, 91 | mpbid 222 |
. . . . . . . . . . 11
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat      |
93 | 48, 92 | ax-mp 5 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat     |
94 | 93 | rgen2w 2925 |
. . . . . . . . 9
        
         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat     |
95 | | eqid 2622 |
. . . . . . . . . 10
        
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      |
96 | 95 | fmpt2 7237 |
. . . . . . . . 9
 
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                         comp          Nat   
Nat   
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                        comp          Nat   
Nat      |
97 | 94, 96 | mpbi 220 |
. . . . . . . 8
        
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                        comp          Nat   
Nat     |
98 | 97 | a1i 11 |
. . . . . . 7
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                                        comp          Nat   
Nat      |
99 | 10, 35, 47, 98 | wunf 9549 |
. . . . . 6
                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                       |
100 | 10, 33, 99 | wunop 9544 |
. . . . 5
  comp                   ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                        |
101 | 10, 27, 31, 100 | wuntp 9533 |
. . . 4
       
          Nat   
 comp           
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)     Nat        Nat                                    comp                      
  |
102 | 18, 101 | eqeltrd 2701 |
. . 3
   |
103 | 1, 13, 16 | fuccat 16630 |
. . 3
   |
104 | 102, 103 | elind 3798 |
. 2
     |
105 | 104, 11 | eleqtrrd 2704 |
1
   |