Step | Hyp | Ref
| Expression |
1 | | isfunc.d |
. . . 4
   |
2 | | isfunc.e |
. . . 4
   |
3 | | fvex 5902 |
. . . . . . . 8
     |
4 | 3 | a1i 11 |
. . . . . . 7
 
       |
5 | | simpl 463 |
. . . . . . . . 9
 
   |
6 | 5 | fveq2d 5896 |
. . . . . . . 8
 
           |
7 | | isfunc.b |
. . . . . . . 8
     |
8 | 6, 7 | syl6eqr 2514 |
. . . . . . 7
 
       |
9 | | simpr 467 |
. . . . . . . . . . 11
       |
10 | | simplr 767 |
. . . . . . . . . . . . 13
       |
11 | 10 | fveq2d 5896 |
. . . . . . . . . . . 12
               |
12 | | isfunc.c |
. . . . . . . . . . . 12
     |
13 | 11, 12 | syl6eqr 2514 |
. . . . . . . . . . 11
           |
14 | 9, 13 | feq23d 5750 |
. . . . . . . . . 10
                     |
15 | | fvex 5902 |
. . . . . . . . . . . 12
     |
16 | 12, 15 | eqeltri 2536 |
. . . . . . . . . . 11
 |
17 | | fvex 5902 |
. . . . . . . . . . . 12
     |
18 | 7, 17 | eqeltri 2536 |
. . . . . . . . . . 11
 |
19 | 16, 18 | elmap 7531 |
. . . . . . . . . 10
  
      |
20 | 14, 19 | syl6bbr 271 |
. . . . . . . . 9
                   |
21 | 9 | sqxpeqd 4882 |
. . . . . . . . . . . 12
           |
22 | 21 | ixpeq1d 7565 |
. . . . . . . . . . 11
                                                                               |
23 | 10 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
             |
24 | | isfunc.j |
. . . . . . . . . . . . . . 15
    |
25 | 23, 24 | syl6eqr 2514 |
. . . . . . . . . . . . . 14
          |
26 | 25 | oveqd 6337 |
. . . . . . . . . . . . 13
                                                  |
27 | | simpll 765 |
. . . . . . . . . . . . . . . 16
       |
28 | 27 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
             |
29 | | isfunc.h |
. . . . . . . . . . . . . . 15
    |
30 | 28, 29 | syl6eqr 2514 |
. . . . . . . . . . . . . 14
          |
31 | 30 | fveq1d 5894 |
. . . . . . . . . . . . 13
      
           |
32 | 26, 31 | oveq12d 6338 |
. . . . . . . . . . . 12
                              
                                  |
33 | 32 | ixpeq2dv 7569 |
. . . . . . . . . . 11
                                                                         |
34 | 22, 33 | eqtrd 2496 |
. . . . . . . . . 10
                                                                         |
35 | 34 | eleq2d 2525 |
. . . . . . . . 9
                                         
                                 |
36 | 27 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
               |
37 | | isfunc.1 |
. . . . . . . . . . . . . . 15
     |
38 | 36, 37 | syl6eqr 2514 |
. . . . . . . . . . . . . 14
          |
39 | 38 | fveq1d 5894 |
. . . . . . . . . . . . 13
            
    |
40 | 39 | fveq2d 5896 |
. . . . . . . . . . . 12
                                 |
41 | 10 | fveq2d 5896 |
. . . . . . . . . . . . . 14
               |
42 | | isfunc.i |
. . . . . . . . . . . . . 14
     |
43 | 41, 42 | syl6eqr 2514 |
. . . . . . . . . . . . 13
           |
44 | 43 | fveq1d 5894 |
. . . . . . . . . . . 12
                           |
45 | 40, 44 | eqeq12d 2477 |
. . . . . . . . . . 11
                                 
                     |
46 | 30 | oveqd 6337 |
. . . . . . . . . . . . . 14
                  |
47 | 30 | oveqd 6337 |
. . . . . . . . . . . . . . 15
                  |
48 | 27 | fveq2d 5896 |
. . . . . . . . . . . . . . . . . . . 20
     comp  comp    |
49 | | isfunc.x |
. . . . . . . . . . . . . . . . . . . 20
comp   |
50 | 48, 49 | syl6eqr 2514 |
. . . . . . . . . . . . . . . . . . 19
     comp   |
51 | 50 | oveqd 6337 |
. . . . . . . . . . . . . . . . . 18
          comp           |
52 | 51 | oveqd 6337 |
. . . . . . . . . . . . . . . . 17
            comp                 |
53 | 52 | fveq2d 5896 |
. . . . . . . . . . . . . . . 16
                   comp                          |
54 | 10 | fveq2d 5896 |
. . . . . . . . . . . . . . . . . . 19
     comp  comp    |
55 | | isfunc.o |
. . . . . . . . . . . . . . . . . . 19
comp   |
56 | 54, 55 | syl6eqr 2514 |
. . . . . . . . . . . . . . . . . 18
     comp    |
57 | 56 | oveqd 6337 |
. . . . . . . . . . . . . . . . 17
                  comp                             |
58 | 57 | oveqd 6337 |
. . . . . . . . . . . . . . . 16
                            comp                                                           |
59 | 53, 58 | eqeq12d 2477 |
. . . . . . . . . . . . . . 15
                    comp                              comp                                                                             |
60 | 47, 59 | raleqbidv 3013 |
. . . . . . . . . . . . . 14
      
                      comp                              comp                  
                                                                |
61 | 46, 60 | raleqbidv 3013 |
. . . . . . . . . . . . 13
      
        
  
                   comp                              comp                  
                                                                      |
62 | 9, 61 | raleqbidv 3013 |
. . . . . . . . . . . 12
      

        
  
                   comp                              comp                  

                                                                      |
63 | 9, 62 | raleqbidv 3013 |
. . . . . . . . . . 11
      


        
  
                   comp                              comp                  


                                                                      |
64 | 45, 63 | anbi12d 722 |
. . . . . . . . . 10
                                    

  
                            comp                              comp                                     


                                                                        |
65 | 9, 64 | raleqbidv 3013 |
. . . . . . . . 9
      
                              

  
                            comp                              comp                                        

     
                                                                 |
66 | 20, 35, 65 | 3anbi123d 1348 |
. . . . . . . 8
              
                             
                                   


                                comp                              comp                   
  
                              
                  


                                                                         |
67 | | df-3an 993 |
. . . . . . . 8
   
                                                 


                                                                     
   
                               
                  


                                                                        |
68 | 66, 67 | syl6bb 269 |
. . . . . . 7
              
                             
                                   


                                comp                              comp                   
   
                               
                  


                                                                         |
69 | 4, 8, 68 | sbcied2 3317 |
. . . . . 6
 
        ![]. ].](_drbrack.gif)         
                             
                                   


                                comp                              comp                   
   
                               
                  


                                                                         |
70 | 69 | opabbidv 4482 |
. . . . 5
 
    
      ![]. ].](_drbrack.gif)         
                             
                                   


                                comp                              comp                        
   
                               
                  


                                                                         |
71 | | df-func 15818 |
. . . . 5
            ![]. ].](_drbrack.gif)         
                             
                                   


                                comp                              comp                       |
72 | | ovex 6348 |
. . . . . . 7
   |
73 | | snex 4658 |
. . . . . . . 8
   |
74 | | ovex 6348 |
. . . . . . . . . 10
                           |
75 | 74 | rgenw 2761 |
. . . . . . . . 9
                               |
76 | | ixpexg 7577 |
. . . . . . . . 9
 
                             
                               |
77 | 75, 76 | ax-mp 5 |
. . . . . . . 8
                               |
78 | 73, 77 | xpex 6627 |
. . . . . . 7
                                   |
79 | 72, 78 | iunex 6805 |
. . . . . 6
                                       |
80 | | simpl 463 |
. . . . . . . . . 10
     
                              
                   


     
                                                              
  
                                 |
81 | 80 | anim2i 577 |
. . . . . . . . 9
         
                              
                   


     
                                                                      
                                  |
82 | 81 | 2eximi 1719 |
. . . . . . . 8
             
                              
                   


     
                                                                           
                                 |
83 | | elopab 4726 |
. . . . . . . 8
         
                              
                   


     
                                                               
           
                               
                   


     
                                                                  |
84 | | eliunxp 4994 |
. . . . . . . 8
                                                 
                                  |
85 | 82, 83, 84 | 3imtr4i 274 |
. . . . . . 7
         
                              
                   


     
                                                                                                        |
86 | 85 | ssriv 3448 |
. . . . . 6
        
                              
                   


     
                                                                                                       |
87 | 79, 86 | ssexi 4564 |
. . . . 5
        
                              
                   


     
                                                                 |
88 | 70, 71, 87 | ovmpt2a 6459 |
. . . 4
 
           
                              
                   


     
                                                                  |
89 | 1, 2, 88 | syl2anc 671 |
. . 3
           
                              
                   


     
                                                                  |
90 | 89 | breqd 4429 |
. 2
     
                                                           


                                                                           |
91 | | brabv 6367 |
. . . 4
     
   
                               
                  


                                                                       
    |
92 | | elex 3066 |
. . . . . 6
     |
93 | | elex 3066 |
. . . . . 6
                              
  |
94 | 92, 93 | anim12i 574 |
. . . . 5
   
                              
    |
95 | 94 | 3adant3 1034 |
. . . 4
   
                                                 


                                                                          |
96 | | simpl 463 |
. . . . . . . 8
 
   |
97 | 96 | eleq1d 2524 |
. . . . . . 7
 
         |
98 | | simpr 467 |
. . . . . . . 8
 
   |
99 | 96 | fveq1d 5894 |
. . . . . . . . . . 11
 
                   |
100 | 96 | fveq1d 5894 |
. . . . . . . . . . 11
 
                   |
101 | 99, 100 | oveq12d 6338 |
. . . . . . . . . 10
 
                                           |
102 | 101 | oveq1d 6335 |
. . . . . . . . 9
 
                                                       |
103 | 102 | ixpeq2dv 7569 |
. . . . . . . 8
 
                                                               |
104 | 98, 103 | eleq12d 2534 |
. . . . . . 7
 
  
                            
                                 |
105 | 98 | oveqd 6337 |
. . . . . . . . . . 11
 
           |
106 | 105 | fveq1d 5894 |
. . . . . . . . . 10
 
                       |
107 | 96 | fveq1d 5894 |
. . . . . . . . . . 11
 
           |
108 | 107 | fveq2d 5896 |
. . . . . . . . . 10
 
                   |
109 | 106, 108 | eqeq12d 2477 |
. . . . . . . . 9
 
                   
                     |
110 | 98 | oveqd 6337 |
. . . . . . . . . . . . 13
 
           |
111 | 110 | fveq1d 5894 |
. . . . . . . . . . . 12
 
                                     |
112 | 96 | fveq1d 5894 |
. . . . . . . . . . . . . . 15
 
           |
113 | 107, 112 | opeq12d 4188 |
. . . . . . . . . . . . . 14
 
                         |
114 | 96 | fveq1d 5894 |
. . . . . . . . . . . . . 14
 
           |
115 | 113, 114 | oveq12d 6338 |
. . . . . . . . . . . . 13
 
                                         |
116 | 98 | oveqd 6337 |
. . . . . . . . . . . . . 14
 
           |
117 | 116 | fveq1d 5894 |
. . . . . . . . . . . . 13
 
                   |
118 | 98 | oveqd 6337 |
. . . . . . . . . . . . . 14
 
           |
119 | 118 | fveq1d 5894 |
. . . . . . . . . . . . 13
 
                   |
120 | 115, 117,
119 | oveq123d 6341 |
. . . . . . . . . . . 12
 
                                                                                 |
121 | 111, 120 | eqeq12d 2477 |
. . . . . . . . . . 11
 
                                                                                                                     |
122 | 121 | 2ralbidv 2844 |
. . . . . . . . . 10
 
                                                                                                                                             |
123 | 122 | 2ralbidv 2844 |
. . . . . . . . 9
 
                                                                         

                                                                      |
124 | 109, 123 | anbi12d 722 |
. . . . . . . 8
 
                    


                                                                    
                  


                                                                        |
125 | 124 | ralbidv 2839 |
. . . . . . 7
 
                     


                                                                    

                  


                                                                        |
126 | 97, 104, 125 | 3anbi123d 1348 |
. . . . . 6
 
    
                              
                  


                                                                     
  
                              
                  


                                                                         |
127 | 67, 126 | syl5bbr 267 |
. . . . 5
 
                                                        


                                                                     
  
                              
                  


                                                                         |
128 | | eqid 2462 |
. . . . 5
        
                              
                   


     
                                                                                                                          


                                                                        |
129 | 127, 128 | brabga 4732 |
. . . 4
 
           
                              
                   


     
                                                                
  
                              
                  


                                                                         |
130 | 91, 95, 129 | pm5.21nii 359 |
. . 3
     
   
                               
                  


                                                                          
                              
                  


                                                                        |
131 | 16, 18 | elmap 7531 |
. . . 4
  
      |
132 | 131 | 3anbi1i 1205 |
. . 3
   
                                                 


                                                                     
                                                       

                                                                        |
133 | 130, 132 | bitri 257 |
. 2
     
   
                               
                  


                                                                             
                             
                  


                                                                        |
134 | 90, 133 | syl6bb 269 |
1
     
                                                       

                                                                         |