Step | Hyp | Ref
| Expression |
1 | | df-ov 6293 |
. 2
  
 TransportTo    TransportTo            |
2 | | opelxpi 4866 |
. . . . . . 7
     
                    |
3 | 2 | 3ad2ant1 1029 |
. . . . . 6
                                      |
4 | | opelxpi 4866 |
. . . . . . 7
     
                    |
5 | 4 | 3ad2ant2 1030 |
. . . . . 6
                                      |
6 | | simp3 1010 |
. . . . . . 7
                         |
7 | | op1stg 6805 |
. . . . . . . 8
     
              |
8 | 7 | 3ad2ant2 1030 |
. . . . . . 7
                                |
9 | | op2ndg 6806 |
. . . . . . . 8
     
              |
10 | 9 | 3ad2ant2 1030 |
. . . . . . 7
                                |
11 | 6, 8, 10 | 3netr4d 2701 |
. . . . . 6
                                       |
12 | 3, 5, 11 | 3jca 1188 |
. . . . 5
                                                                   |
13 | 8 | opeq1d 4172 |
. . . . . . . . 9
                                      |
14 | 10, 13 | breq12d 4415 |
. . . . . . . 8
                                        
 
    |
15 | 10 | opeq1d 4172 |
. . . . . . . . 9
                                      |
16 | 15 | breq1d 4412 |
. . . . . . . 8
                                  Cgr      Cgr      |
17 | 14, 16 | anbi12d 717 |
. . . . . . 7
                                                    Cgr      
    Cgr       |
18 | 17 | riotabidv 6254 |
. . . . . 6
                                                          Cgr      
     
  
   Cgr       |
19 | 18 | eqcomd 2457 |
. . . . 5
                              
  
   Cgr      
                                 Cgr       |
20 | 12, 19 | jca 535 |
. . . 4
                                                                 
              Cgr      
                                 Cgr        |
21 | | fveq2 5865 |
. . . . . . . . 9
           |
22 | 21 | sqxpeqd 4860 |
. . . . . . . 8
                       |
23 | 22 | eleq2d 2514 |
. . . . . . 7
                               |
24 | 22 | eleq2d 2514 |
. . . . . . 7
                               |
25 | 23, 24 | 3anbi12d 1340 |
. . . . . 6
                                                           
                             |
26 | 21 | riotaeqdv 6253 |
. . . . . . 7
                                    Cgr      
                                 Cgr       |
27 | 26 | eqeq2d 2461 |
. . . . . 6
            
   Cgr      
                                 Cgr    
              Cgr      
                                 Cgr        |
28 | 25, 27 | anbi12d 717 |
. . . . 5
                  
                         
              Cgr      
                                 Cgr     
                                                  
  
   Cgr      
                                 Cgr         |
29 | 28 | rspcev 3150 |
. . . 4
                  
                         
              Cgr      
                                 Cgr                        
                         
              Cgr      
                                 Cgr        |
30 | 20, 29 | sylan2 477 |
. . 3
       
                 
                
                         
              Cgr      
                                 Cgr        |
31 | | df-br 4403 |
. . . . 5
          TransportTo 
     
  
   Cgr    
                         Cgr      TransportTo |
32 | | df-transport 30797 |
. . . . . 6
TransportTo      
                                
                          Cgr     |
33 | 32 | eleq2i 2521 |
. . . . 5
                          Cgr      TransportTo
                         Cgr           
                                
                          Cgr      |
34 | | opex 4664 |
. . . . . 6
    |
35 | | opex 4664 |
. . . . . 6
    |
36 | | riotaex 6256 |
. . . . . 6
              Cgr      |
37 | | eleq1 2517 |
. . . . . . . . . 10
                               |
38 | 37 | 3anbi1d 1343 |
. . . . . . . . 9
                                  
                                    |
39 | | breq2 4406 |
. . . . . . . . . . . 12
            Cgr
       Cgr      |
40 | 39 | anbi2d 710 |
. . . . . . . . . . 11
                        Cgr
                   Cgr       |
41 | 40 | riotabidv 6254 |
. . . . . . . . . 10
                      
       Cgr                    
       Cgr       |
42 | 41 | eqeq2d 2461 |
. . . . . . . . 9
                
              Cgr 
           
              Cgr        |
43 | 38, 42 | anbi12d 717 |
. . . . . . . 8
                
                                     
       Cgr      
                             
                          Cgr         |
44 | 43 | rexbidv 2901 |
. . . . . . 7
                                    
                          Cgr   
              
                                     
       Cgr         |
45 | | eleq1 2517 |
. . . . . . . . . 10
                               |
46 | | fveq2 5865 |
. . . . . . . . . . 11
                 |
47 | | fveq2 5865 |
. . . . . . . . . . 11
                 |
48 | 46, 47 | neeq12d 2685 |
. . . . . . . . . 10
            
                 |
49 | 45, 48 | 3anbi23d 1342 |
. . . . . . . . 9
       
                             
                                             |
50 | 46 | opeq1d 4172 |
. . . . . . . . . . . . 13
                       |
51 | 47, 50 | breq12d 4415 |
. . . . . . . . . . . 12
               
                    |
52 | 47 | opeq1d 4172 |
. . . . . . . . . . . . 13
                       |
53 | 52 | breq1d 4412 |
. . . . . . . . . . . 12
            Cgr             Cgr      |
54 | 51, 53 | anbi12d 717 |
. . . . . . . . . . 11
                        Cgr                                Cgr       |
55 | 54 | riotabidv 6254 |
. . . . . . . . . 10
                      
       Cgr      
                                 Cgr       |
56 | 55 | eqeq2d 2461 |
. . . . . . . . 9
                
              Cgr    
                                   Cgr        |
57 | 49, 56 | anbi12d 717 |
. . . . . . . 8
                                      
                          Cgr     
                                                         
                    Cgr         |
58 | 57 | rexbidv 2901 |
. . . . . . 7
         
                             
                          Cgr     
    
                                                     
                    Cgr         |
59 | | eqeq1 2455 |
. . . . . . . . 9
          
    Cgr    
               
                    Cgr    
              Cgr      
                                 Cgr        |
60 | 59 | anbi2d 710 |
. . . . . . . 8
          
    Cgr    
                                           
                                   Cgr     
                                                  
  
   Cgr      
                                 Cgr         |
61 | 60 | rexbidv 2901 |
. . . . . . 7
          
    Cgr    
 
                                          
                                   Cgr     
    
                                              
  
   Cgr      
                                 Cgr         |
62 | 44, 58, 61 | eloprabg 6384 |
. . . . . 6
    
             
   Cgr                                Cgr           
                                
                          Cgr                     
                         
              Cgr      
                                 Cgr         |
63 | 34, 35, 36, 62 | mp3an 1364 |
. . . . 5
                          Cgr           
                                
                          Cgr                     
                         
              Cgr      
                                 Cgr        |
64 | 31, 33, 63 | 3bitri 275 |
. . . 4
          TransportTo 
     
  
   Cgr    
    
                                              
  
   Cgr      
                                 Cgr        |
65 | | funtransport 30798 |
. . . . 5
TransportTo |
66 | | funbrfv 5903 |
. . . . 5
 TransportTo           TransportTo          
   Cgr     TransportTo            
     
  
   Cgr        |
67 | 65, 66 | ax-mp 5 |
. . . 4
          TransportTo 
     
  
   Cgr     TransportTo            
     
  
   Cgr       |
68 | 64, 67 | sylbir 217 |
. . 3
                                            
              Cgr      
                                 Cgr      TransportTo            
     
  
   Cgr       |
69 | 30, 68 | syl 17 |
. 2
       
                 TransportTo            
     
  
   Cgr       |
70 | 1, 69 | syl5eq 2497 |
1
       
                     TransportTo             
    Cgr       |