Step | Hyp | Ref
| Expression |
1 | | eqid 2471 |
. . . 4
         |
2 | | cofucl.f |
. . . 4
     |
3 | | cofucl.g |
. . . 4
     |
4 | 1, 2, 3 | cofuval 15865 |
. . 3
  func
                                                             |
5 | 1, 2, 3 | cofu1st 15866 |
. . . 4
     func               |
6 | 4 | fveq2d 5883 |
. . . . 5
     func                       
                                           |
7 | | fvex 5889 |
. . . . . . 7
     |
8 | | fvex 5889 |
. . . . . . 7
     |
9 | 7, 8 | coex 6764 |
. . . . . 6
           |
10 | | fvex 5889 |
. . . . . . 7
     |
11 | 10, 10 | mpt2ex 6889 |
. . . . . 6
                                              |
12 | 9, 11 | op2nd 6821 |
. . . . 5
                                                                                                            |
13 | 6, 12 | syl6eq 2521 |
. . . 4
     func        
                                         |
14 | 5, 13 | opeq12d 4166 |
. . 3
      func        func                                                                |
15 | 4, 14 | eqtr4d 2508 |
. 2
  func
      func        func      |
16 | | eqid 2471 |
. . . . . . 7
         |
17 | | eqid 2471 |
. . . . . . 7
         |
18 | | relfunc 15845 |
. . . . . . . 8
   |
19 | | 1st2ndbr 6861 |
. . . . . . . 8
            
        |
20 | 18, 3, 19 | sylancr 676 |
. . . . . . 7
               |
21 | 16, 17, 20 | funcf1 15849 |
. . . . . 6
                   |
22 | | relfunc 15845 |
. . . . . . . 8
   |
23 | | 1st2ndbr 6861 |
. . . . . . . 8
            
        |
24 | 22, 2, 23 | sylancr 676 |
. . . . . . 7
               |
25 | 1, 16, 24 | funcf1 15849 |
. . . . . 6
                   |
26 | | fco 5751 |
. . . . . 6
                                                           |
27 | 21, 25, 26 | syl2anc 673 |
. . . . 5
                         |
28 | 5 | feq1d 5724 |
. . . . 5
      func                                        |
29 | 27, 28 | mpbird 240 |
. . . 4
     func                 |
30 | | eqid 2471 |
. . . . . . 7
                                                                                           |
31 | | ovex 6336 |
. . . . . . . 8
                         |
32 | | ovex 6336 |
. . . . . . . 8
         |
33 | 31, 32 | coex 6764 |
. . . . . . 7
                                   |
34 | 30, 33 | fnmpt2i 6881 |
. . . . . 6
                                                        |
35 | 13 | fneq1d 5676 |
. . . . . 6
      func            
                                                          |
36 | 34, 35 | mpbiri 241 |
. . . . 5
     func               |
37 | | eqid 2471 |
. . . . . . . . . . 11
       |
38 | | eqid 2471 |
. . . . . . . . . . 11
       |
39 | 20 | adantr 472 |
. . . . . . . . . . 11
 
    
           
        |
40 | 25 | adantr 472 |
. . . . . . . . . . . 12
 
    
                        |
41 | | simprl 772 |
. . . . . . . . . . . 12
 
    
            |
42 | 40, 41 | ffvelrnd 6038 |
. . . . . . . . . . 11
 
    
                    |
43 | | simprr 774 |
. . . . . . . . . . . 12
 
    
            |
44 | 40, 43 | ffvelrnd 6038 |
. . . . . . . . . . 11
 
    
                    |
45 | 16, 37, 38, 39, 42, 44 | funcf2 15851 |
. . . . . . . . . 10
 
    
                                          
                                                       |
46 | | eqid 2471 |
. . . . . . . . . . 11
       |
47 | 24 | adantr 472 |
. . . . . . . . . . 11
 
    
           
        |
48 | 1, 46, 37, 47, 41, 43 | funcf2 15851 |
. . . . . . . . . 10
 
    
                                                  |
49 | | fco 5751 |
. . . . . . . . . 10
                                      
                                                                                  
                                                                                                   |
50 | 45, 48, 49 | syl2anc 673 |
. . . . . . . . 9
 
    
                                                                                            |
51 | | ovex 6336 |
. . . . . . . . . 10
                                        |
52 | | ovex 6336 |
. . . . . . . . . 10
        |
53 | 51, 52 | elmap 7518 |
. . . . . . . . 9
                                                                                  
                                                                                      |
54 | 50, 53 | sylibr 217 |
. . . . . . . 8
 
    
                                                                                          |
55 | 2 | adantr 472 |
. . . . . . . . 9
 
    
          |
56 | 3 | adantr 472 |
. . . . . . . . 9
 
    
          |
57 | 1, 55, 56, 41, 43 | cofu2nd 15868 |
. . . . . . . 8
 
    
            func                                         |
58 | 1, 55, 56, 41 | cofu1 15867 |
. . . . . . . . . 10
 
    
           func                        |
59 | 1, 55, 56, 43 | cofu1 15867 |
. . . . . . . . . 10
 
    
           func                        |
60 | 58, 59 | oveq12d 6326 |
. . . . . . . . 9
 
    
            func                func                                                |
61 | 60 | oveq1d 6323 |
. . . . . . . 8
 
    
             func
      
        func                                                                 |
62 | 54, 57, 61 | 3eltr4d 2564 |
. . . . . . 7
 
    
            func            func                func                 |
63 | 62 | ralrimivva 2814 |
. . . . . 6
       
           func            func                func                 |
64 | | fveq2 5879 |
. . . . . . . . 9
         func
          func
          |
65 | | df-ov 6311 |
. . . . . . . . 9
      func          func          |
66 | 64, 65 | syl6eqr 2523 |
. . . . . . . 8
         func
           func       |
67 | | vex 3034 |
. . . . . . . . . . . 12
 |
68 | | vex 3034 |
. . . . . . . . . . . 12
 |
69 | 67, 68 | op1std 6822 |
. . . . . . . . . . 11
          |
70 | 69 | fveq2d 5883 |
. . . . . . . . . 10
         func
              func        |
71 | 67, 68 | op2ndd 6823 |
. . . . . . . . . . 11
          |
72 | 71 | fveq2d 5883 |
. . . . . . . . . 10
         func
              func        |
73 | 70, 72 | oveq12d 6326 |
. . . . . . . . 9
          func                    func
                func                func         |
74 | | fveq2 5879 |
. . . . . . . . . 10
                       |
75 | | df-ov 6311 |
. . . . . . . . . 10
                  |
76 | 74, 75 | syl6eqr 2523 |
. . . . . . . . 9
                    |
77 | 73, 76 | oveq12d 6326 |
. . . . . . . 8
           func                    func
                         func
      
        func                 |
78 | 66, 77 | eleq12d 2543 |
. . . . . . 7
          func             func
                   func            
            func
           func                func                  |
79 | 78 | ralxp 4981 |
. . . . . 6
 
                func             func
                   func            
      
     
           func            func                func                 |
80 | 63, 79 | sylibr 217 |
. . . . 5
                  func             func
                   func            
        |
81 | | fvex 5889 |
. . . . . 6
    func
   |
82 | 81 | elixp 7547 |
. . . . 5
     func   
                  func                    func
                 
     func             
                func             func
                   func            
         |
83 | 36, 80, 82 | sylanbrc 677 |
. . . 4
     func   
                  func                    func
                    |
84 | | eqid 2471 |
. . . . . . . . . 10
         |
85 | | eqid 2471 |
. . . . . . . . . 10
         |
86 | 24 | adantr 472 |
. . . . . . . . . 10
 
    
              |
87 | | simpr 468 |
. . . . . . . . . 10
 
    
      |
88 | 1, 84, 85, 86, 87 | funcid 15853 |
. . . . . . . . 9
 
    
                                      |
89 | 88 | fveq2d 5883 |
. . . . . . . 8
 
    
                                                                                              |
90 | | eqid 2471 |
. . . . . . . . 9
         |
91 | 20 | adantr 472 |
. . . . . . . . 9
 
    
              |
92 | 25 | ffvelrnda 6037 |
. . . . . . . . 9
 
    
              |
93 | 16, 85, 90, 91, 92 | funcid 15853 |
. . . . . . . 8
 
    
                                                                      |
94 | 89, 93 | eqtrd 2505 |
. . . . . . 7
 
    
                                                                          |
95 | 2 | adantr 472 |
. . . . . . . 8
 
    

   |
96 | 3 | adantr 472 |
. . . . . . . 8
 
    

   |
97 | | funcrcl 15846 |
. . . . . . . . . . . 12
  
    |
98 | 2, 97 | syl 17 |
. . . . . . . . . . 11
     |
99 | 98 | simpld 466 |
. . . . . . . . . 10
   |
100 | 99 | adantr 472 |
. . . . . . . . 9
 
    
  |
101 | 1, 46, 84, 100, 87 | catidcl 15666 |
. . . . . . . 8
 
    
                 |
102 | 1, 95, 96, 87, 87, 46, 101 | cofu2 15869 |
. . . . . . 7
 
    
       func                                                                  |
103 | 1, 95, 96, 87 | cofu1 15867 |
. . . . . . . 8
 
    
     func                        |
104 | 103 | fveq2d 5883 |
. . . . . . 7
 
    
            func                                 |
105 | 94, 102, 104 | 3eqtr4d 2515 |
. . . . . 6
 
    
       func                            func         |
106 | 86 | adantr 472 |
. . . . . . . . . . . . 13
             
                            
        |
107 | | simplr 770 |
. . . . . . . . . . . . 13
             
                             |
108 | | simprlr 781 |
. . . . . . . . . . . . 13
             
                             |
109 | 1, 46, 37, 106, 107, 108 | funcf2 15851 |
. . . . . . . . . . . 12
             
                                                                   |
110 | | eqid 2471 |
. . . . . . . . . . . . 13
comp  comp   |
111 | 100 | adantr 472 |
. . . . . . . . . . . . 13
             
                         |
112 | | simprll 780 |
. . . . . . . . . . . . 13
             
                             |
113 | | simprrl 782 |
. . . . . . . . . . . . 13
             
                                |
114 | | simprrr 783 |
. . . . . . . . . . . . 13
             
                                |
115 | 1, 46, 110, 111, 107, 112, 108, 113, 114 | catcocl 15669 |
. . . . . . . . . . . 12
             
                              comp               |
116 | | fvco3 5957 |
. . . . . . . . . . . 12
                               
           
       comp                                                          comp                                                    comp          |
117 | 109, 115,
116 | syl2anc 673 |
. . . . . . . . . . 11
             
                                                                   comp                                                    comp          |
118 | | eqid 2471 |
. . . . . . . . . . . . 13
comp  comp   |
119 | 1, 46, 110, 118, 106, 107, 112, 108, 113, 114 | funcco 15854 |
. . . . . . . . . . . 12
             
                                         comp                                          comp                            |
120 | 119 | fveq2d 5883 |
. . . . . . . . . . 11
             
                                                                    comp                                                                      comp                             |
121 | | eqid 2471 |
. . . . . . . . . . . 12
comp  comp   |
122 | 91 | adantr 472 |
. . . . . . . . . . . 12
             
                            
        |
123 | 92 | adantr 472 |
. . . . . . . . . . . 12
             
                                     |
124 | 25 | adantr 472 |
. . . . . . . . . . . . . 14
 
    
                  |
125 | 124 | adantr 472 |
. . . . . . . . . . . . 13
             
                                         |
126 | 125, 112 | ffvelrnd 6038 |
. . . . . . . . . . . 12
             
                                     |
127 | 125, 108 | ffvelrnd 6038 |
. . . . . . . . . . . 12
             
                                     |
128 | 1, 46, 37, 106, 107, 112 | funcf2 15851 |
. . . . . . . . . . . . 13
             
                                                                   |
129 | 128, 113 | ffvelrnd 6038 |
. . . . . . . . . . . 12
             
                                                            |
130 | 1, 46, 37, 106, 112, 108 | funcf2 15851 |
. . . . . . . . . . . . 13
             
                                                                   |
131 | 130, 114 | ffvelrnd 6038 |
. . . . . . . . . . . 12
             
                                                            |
132 | 16, 37, 118, 121, 122, 123, 126, 127, 129, 131 | funcco 15854 |
. . . . . . . . . . 11
             
                                                                                     comp                                                                                                          comp                                                                |
133 | 117, 120,
132 | 3eqtrd 2509 |
. . . . . . . . . 10
             
                                                                   comp                                                                                      comp                                                                |
134 | 95 | adantr 472 |
. . . . . . . . . . . 12
             
                           |
135 | 96 | adantr 472 |
. . . . . . . . . . . 12
             
                           |
136 | 1, 134, 135, 107, 108 | cofu2nd 15868 |
. . . . . . . . . . 11
             
                             func                                         |
137 | 136 | fveq1d 5881 |
. . . . . . . . . 10
             
                              func
             comp                                                   comp         |
138 | 103 | adantr 472 |
. . . . . . . . . . . . 13
             
                            func                        |
139 | 1, 134, 135, 112 | cofu1 15867 |
. . . . . . . . . . . . 13
             
                            func                        |
140 | 138, 139 | opeq12d 4166 |
. . . . . . . . . . . 12
             
                             func            func                                            |
141 | 1, 134, 135, 108 | cofu1 15867 |
. . . . . . . . . . . 12
             
                            func                        |
142 | 140, 141 | oveq12d 6326 |
. . . . . . . . . . 11
             
                              func            func        comp        func                                            comp                      |
143 | 1, 134, 135, 112, 108, 46, 114 | cofu2 15869 |
. . . . . . . . . . 11
             
                              func
                                                 |
144 | 1, 134, 135, 107, 112, 46, 113 | cofu2 15869 |
. . . . . . . . . . 11
             
                              func
                                                 |
145 | 142, 143,
144 | oveq123d 6329 |
. . . . . . . . . 10
             
                               func                func
           func
       comp        func               func
                                                                                       comp                                                                |
146 | 133, 137,
145 | 3eqtr4d 2515 |
. . . . . . . . 9
             
                              func
             comp               func
               func            func        comp        func               func
          |
147 | 146 | anassrs 660 |
. . . . . . . 8
   
         
                              func
             comp               func
               func            func        comp        func               func
          |
148 | 147 | ralrimivva 2814 |
. . . . . . 7
                   
        
  
            func              comp               func
               func            func        comp        func               func
          |
149 | 148 | ralrimivva 2814 |
. . . . . 6
 
    
                                     func
             comp               func
               func            func        comp        func               func
          |
150 | 105, 149 | jca 541 |
. . . . 5
 
    
        func
                           func                                            func
             comp               func
               func            func        comp        func               func
           |
151 | 150 | ralrimiva 2809 |
. . . 4
               func                            func                                            func
             comp               func
               func            func        comp        func               func
           |
152 | | funcrcl 15846 |
. . . . . . 7
  
    |
153 | 3, 152 | syl 17 |
. . . . . 6
     |
154 | 153 | simprd 470 |
. . . . 5
   |
155 | 1, 17, 46, 38, 84, 90, 110, 121, 99, 154 | isfunc 15847 |
. . . 4
      func    
      func  
     func                   func                      func
                   func            
                    func                            func                                            func
             comp               func
               func            func        comp        func               func
             |
156 | 29, 83, 151, 155 | mpbir3and 1213 |
. . 3
     func    
      func     |
157 | | df-br 4396 |
. . 3
     func    
      func  
     func
       func
       |
158 | 156, 157 | sylib 201 |
. 2
      func        func        |
159 | 15, 158 | eqeltrd 2549 |
1
  func
     |