Step | Hyp | Ref
| Expression |
1 | | mptexg 6159 |
. . 3
               |
2 | 1 | 3ad2ant2 1036 |
. 2
 
                            |
3 | | ffvelrn 6042 |
. . . . . . . . . 10
             
               |
4 | 3 | expcom 441 |
. . . . . . . . 9
                             |
5 | 4 | ralimdv 2809 |
. . . . . . . 8
  
            
               |
6 | 5 | impcom 436 |
. . . . . . 7
              
                |
7 | 6 | 3ad2antl3 1178 |
. . . . . 6
  
              

              |
8 | | fveq2 5887 |
. . . . . . . . 9
           |
9 | 8 | fveq1d 5889 |
. . . . . . . 8
                   |
10 | | fveq2 5887 |
. . . . . . . 8
           |
11 | 9, 10 | eleq12d 2533 |
. . . . . . 7
             
               |
12 | 11 | cbvralv 3030 |
. . . . . 6
 
                           |
13 | 7, 12 | sylib 201 |
. . . . 5
  
              

              |
14 | | simpl1 1017 |
. . . . . 6
  
              
  |
15 | | mptelixpg 7584 |
. . . . . 6
            
                    |
16 | 14, 15 | syl 17 |
. . . . 5
  
              
           
   

               |
17 | 13, 16 | mpbird 240 |
. . . 4
  
              

                |
18 | | upixp.1 |
. . . . 5
      |
19 | | fveq2 5887 |
. . . . . 6
           |
20 | 19 | cbvixpv 7565 |
. . . . 5

    
     |
21 | 18, 20 | eqtri 2483 |
. . . 4
      |
22 | 17, 21 | syl6eleqr 2550 |
. . 3
  
              

           |
23 | | eqid 2461 |
. . 3
                         |
24 | 22, 23 | fmptd 6068 |
. 2
 
                                |
25 | | nfv 1771 |
. . . 4
  |
26 | | nfv 1771 |
. . . 4
  |
27 | | nfra1 2780 |
. . . 4
                |
28 | 25, 26, 27 | nf3an 2023 |
. . 3
  
               |
29 | | fveq2 5887 |
. . . . . . . . 9
           |
30 | 29 | fveq1d 5889 |
. . . . . . . 8
                   |
31 | | eqid 2461 |
. . . . . . . 8
                     |
32 | | fvex 5897 |
. . . . . . . 8
         |
33 | 30, 31, 32 | fvmpt3i 5975 |
. . . . . . 7
                         |
34 | 33 | adantl 472 |
. . . . . 6
  
              
                        |
35 | 34 | mpteq2dv 4503 |
. . . . 5
  
              

                           |
36 | 22 | adantlr 726 |
. . . . . 6
    
                           |
37 | | eqidd 2462 |
. . . . . 6
  
              

                         |
38 | | fveq2 5887 |
. . . . . . . . 9
           |
39 | 38 | mpteq2dv 4503 |
. . . . . . . 8
               |
40 | | upixp.2 |
. . . . . . . 8
         |
41 | | fvex 5897 |
. . . . . . . . . . . 12
     |
42 | 41 | rgenw 2760 |
. . . . . . . . . . 11

     |
43 | | ixpexg 7571 |
. . . . . . . . . . 11
 
   
       |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . 10

     |
45 | 18, 44 | eqeltri 2535 |
. . . . . . . . 9
 |
46 | 45 | mptex 6160 |
. . . . . . . 8
       |
47 | 39, 40, 46 | fvmpt3i 5975 |
. . . . . . 7
             |
48 | 47 | adantl 472 |
. . . . . 6
  
              
            |
49 | | fveq1 5886 |
. . . . . 6
                               |
50 | 36, 37, 48, 49 | fmptco 6079 |
. . . . 5
  
              
                                    |
51 | | rsp 2765 |
. . . . . . . 8
 
                            |
52 | 51 | 3ad2ant3 1037 |
. . . . . . 7
 
              
               |
53 | 52 | imp 435 |
. . . . . 6
  
              
              |
54 | 53 | feqmptd 5940 |
. . . . 5
  
              
                |
55 | 35, 50, 54 | 3eqtr4rd 2506 |
. . . 4
  
              
                        |
56 | 55 | ex 440 |
. . 3
 
              
                         |
57 | 28, 56 | ralrimi 2799 |
. 2
 
                                       |
58 | | simprl 769 |
. . . . . 6
  
                   
                  |
59 | 58 | feqmptd 5940 |
. . . . 5
  
                   
                    |
60 | | simplrr 776 |
. . . . . . . . . . 11
    
                               

            |
61 | | fveq2 5887 |
. . . . . . . . . . . . . 14
           |
62 | 61 | coeq1d 5014 |
. . . . . . . . . . . . 13
               |
63 | 8, 62 | eqeq12d 2476 |
. . . . . . . . . . . 12
           
             |
64 | 63 | rspccva 3160 |
. . . . . . . . . . 11
                          |
65 | 60, 64 | sylan 478 |
. . . . . . . . . 10
    

                               
             |
66 | 65 | fveq1d 5889 |
. . . . . . . . 9
    

                               
                     |
67 | | fvco3 5964 |
. . . . . . . . . . 11
     
                         |
68 | 58, 67 | sylan 478 |
. . . . . . . . . 10
    
                               
                        |
69 | 68 | adantr 471 |
. . . . . . . . 9
    

                               
                         |
70 | | fveq2 5887 |
. . . . . . . . . . . . . 14
           |
71 | 70 | mpteq2dv 4503 |
. . . . . . . . . . . . 13
               |
72 | 71, 40, 46 | fvmpt3i 5975 |
. . . . . . . . . . . 12
             |
73 | 72 | adantl 472 |
. . . . . . . . . . 11
    

                               
             |
74 | 73 | fveq1d 5889 |
. . . . . . . . . 10
    

                               
                             |
75 | | ffvelrn 6042 |
. . . . . . . . . . . . 13
     
       |
76 | 58, 75 | sylan 478 |
. . . . . . . . . . . 12
    
                               
      |
77 | | fveq1 5886 |
. . . . . . . . . . . . 13
                   |
78 | | eqid 2461 |
. . . . . . . . . . . . 13
             |
79 | | fvex 5897 |
. . . . . . . . . . . . 13
     |
80 | 77, 78, 79 | fvmpt3i 5975 |
. . . . . . . . . . . 12
                             |
81 | 76, 80 | syl 17 |
. . . . . . . . . . 11
    
                               
                        |
82 | 81 | adantr 471 |
. . . . . . . . . 10
    

                               
                         |
83 | 74, 82 | eqtrd 2495 |
. . . . . . . . 9
    

                               
                       |
84 | 66, 69, 83 | 3eqtrd 2499 |
. . . . . . . 8
    

                               
                   |
85 | 84 | mpteq2dva 4502 |
. . . . . . 7
    
                               

                     |
86 | 76, 18 | syl6eleq 2549 |
. . . . . . . . 9
    
                               
    
      |
87 | | ixpfn 7553 |
. . . . . . . . 9
                |
88 | 86, 87 | syl 17 |
. . . . . . . 8
    
                               
      |
89 | | dffn5 5932 |
. . . . . . . 8
    
                |
90 | 88, 89 | sylib 201 |
. . . . . . 7
    
                               
                |
91 | 85, 90 | eqtr4d 2498 |
. . . . . 6
    
                               

               |
92 | 91 | mpteq2dva 4502 |
. . . . 5
  
                   
                                |
93 | 59, 92 | eqtr4d 2498 |
. . . 4
  
                   
                          |
94 | 93 | ex 440 |
. . 3
 
                               

              |
95 | 94 | alrimiv 1783 |
. 2
 
                                 

              |
96 | | feq1 5731 |
. . . 4
                 

                  |
97 | | coeq2 5011 |
. . . . . 6
                                       |
98 | 97 | eqeq2d 2471 |
. . . . 5
                                                 |
99 | 98 | ralbidv 2838 |
. . . 4
              
          
                         |
100 | 96, 99 | anbi12d 722 |
. . 3
                              
                                            |
101 | 100 | eqeu 3220 |
. 2
             
                                                            

                    
             |
102 | 2, 24, 57, 95, 101 | syl121anc 1281 |
1
 
                                   |