Step | Hyp | Ref
| Expression |
1 | | catidd.2 |
. . . . . . . . . . 11
 

               |
2 | 1 | ex 436 |
. . . . . . . . . 10
                  |
3 | | catidd.b |
. . . . . . . . . . . 12
       |
4 | 3 | eleq2d 2514 |
. . . . . . . . . . 11
         |
5 | 3 | eleq2d 2514 |
. . . . . . . . . . 11
         |
6 | | catidd.h |
. . . . . . . . . . . . 13
      |
7 | 6 | oveqd 6307 |
. . . . . . . . . . . 12
              |
8 | 7 | eleq2d 2514 |
. . . . . . . . . . 11
                |
9 | 4, 5, 8 | 3anbi123d 1339 |
. . . . . . . . . 10
       
    
   
           |
10 | | catidd.o |
. . . . . . . . . . . . 13
 comp    |
11 | 10 | oveqd 6307 |
. . . . . . . . . . . 12
           comp      |
12 | 11 | oveqd 6307 |
. . . . . . . . . . 11
             comp        |
13 | 12 | eqeq1d 2453 |
. . . . . . . . . 10
        
     comp         |
14 | 2, 9, 13 | 3imtr3d 271 |
. . . . . . . . 9
      
   
             comp         |
15 | 14 | 3expd 1226 |
. . . . . . . 8
                        comp           |
16 | 15 | imp41 598 |
. . . . . . 7
   
    
    
  
          comp        |
17 | 16 | ralrimiva 2802 |
. . . . . 6
                           comp        |
18 | | catidd.3 |
. . . . . . . . . . 11
 

               |
19 | 18 | ex 436 |
. . . . . . . . . 10
             
    |
20 | 6 | oveqd 6307 |
. . . . . . . . . . . 12
              |
21 | 20 | eleq2d 2514 |
. . . . . . . . . . 11
                |
22 | 4, 5, 21 | 3anbi123d 1339 |
. . . . . . . . . 10
       
    
   
           |
23 | 10 | oveqd 6307 |
. . . . . . . . . . . 12
           comp      |
24 | 23 | oveqd 6307 |
. . . . . . . . . . 11
               comp      |
25 | 24 | eqeq1d 2453 |
. . . . . . . . . 10
        
       comp       |
26 | 19, 22, 25 | 3imtr3d 271 |
. . . . . . . . 9
      
   
               comp       |
27 | 26 | 3expd 1226 |
. . . . . . . 8
                          comp         |
28 | 27 | imp41 598 |
. . . . . . 7
   
    
    
  
            comp      |
29 | 28 | ralrimiva 2802 |
. . . . . 6
                             comp      |
30 | 17, 29 | jca 535 |
. . . . 5
              
             comp                      comp       |
31 | 30 | ralrimiva 2802 |
. . . 4
 
    
                     comp                      comp       |
32 | | catidd.1 |
. . . . . . . 8
 
       |
33 | 32 | ex 436 |
. . . . . . 7
         |
34 | 6 | oveqd 6307 |
. . . . . . . 8
              |
35 | 34 | eleq2d 2514 |
. . . . . . 7
    
  
       |
36 | 33, 4, 35 | 3imtr3d 271 |
. . . . . 6
                |
37 | 36 | imp 431 |
. . . . 5
 
    
         |
38 | | eqid 2451 |
. . . . . 6
         |
39 | | eqid 2451 |
. . . . . 6
       |
40 | | eqid 2451 |
. . . . . 6
comp  comp   |
41 | | catidd.c |
. . . . . . 7
   |
42 | 41 | adantr 467 |
. . . . . 6
 
    
  |
43 | | simpr 463 |
. . . . . 6
 
    
      |
44 | 38, 39, 40, 42, 43 | catideu 15581 |
. . . . 5
 
    
                                comp                      comp         |
45 | | oveq1 6297 |
. . . . . . . . . 10
        comp           comp        |
46 | 45 | eqeq1d 2453 |
. . . . . . . . 9
         comp           comp         |
47 | 46 | ralbidv 2827 |
. . . . . . . 8
  
               comp     
              comp         |
48 | | oveq2 6298 |
. . . . . . . . . 10
        comp             comp      |
49 | 48 | eqeq1d 2453 |
. . . . . . . . 9
         comp             comp       |
50 | 49 | ralbidv 2827 |
. . . . . . . 8
  
               comp     
                comp       |
51 | 47, 50 | anbi12d 717 |
. . . . . . 7
                   comp                      comp                      comp                      comp        |
52 | 51 | ralbidv 2827 |
. . . . . 6
  
                      comp                      comp       
                    comp                      comp        |
53 | 52 | riota2 6274 |
. . . . 5
        
        
      
  
            comp      
  
            comp                              comp                      comp                                      comp                      comp          |
54 | 37, 44, 53 | syl2anc 667 |
. . . 4
 
    
 
      
  
          comp      
  
            comp    
                                 comp                      comp          |
55 | 31, 54 | mpbid 214 |
. . 3
 
    
                                 comp                      comp         |
56 | 55 | mpteq2dva 4489 |
. 2
                
      
  
            comp      
  
            comp             
  |
57 | | eqid 2451 |
. . 3
         |
58 | 38, 39, 40, 41, 57 | cidfval 15582 |
. 2
                                           comp                      comp           |
59 | 3 | mpteq1d 4484 |
. 2
         |
60 | 56, 58, 59 | 3eqtr4d 2495 |
1
        |