Step | Hyp | Ref
| Expression |
1 | | eluzelz 11168 |
. . . . . . . . . . . . 13
    
  |
2 | 1 | adantl 468 |
. . . . . . . . . . . 12
  
        
  |
3 | | nfra1 2769 |
. . . . . . . . . . . . . . . . 17
  
     |
4 | | rsp 2754 |
. . . . . . . . . . . . . . . . . . . . 21
 
   

       |
5 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
  
             |
6 | | ifeq1 3885 |
. . . . . . . . . . . . . . . . . . . 20
       
                 |
7 | 5, 6 | syl6 34 |
. . . . . . . . . . . . . . . . . . 19
  
        
                  |
8 | | iffalse 3890 |
. . . . . . . . . . . . . . . . . . . 20
   
          |
9 | | iffalse 3890 |
. . . . . . . . . . . . . . . . . . . 20
   
          |
10 | 8, 9 | eqtr4d 2488 |
. . . . . . . . . . . . . . . . . . 19
   
                 |
11 | 7, 10 | pm2.61d1 163 |
. . . . . . . . . . . . . . . . . 18
  
       
                 |
12 | | fvif 5876 |
. . . . . . . . . . . . . . . . . 18
                 |
13 | | fvif 5876 |
. . . . . . . . . . . . . . . . . 18
                 |
14 | 11, 12, 13 | 3eqtr4g 2510 |
. . . . . . . . . . . . . . . . 17
  
                     |
15 | 3, 14 | mpteq2da 4488 |
. . . . . . . . . . . . . . . 16
 
   
              
     |
16 | 15 | adantr 467 |
. . . . . . . . . . . . . . 15
  
        
              
     |
17 | 16 | fveq1d 5867 |
. . . . . . . . . . . . . 14
  
        
      
            
        |
18 | 17 | adantlr 721 |
. . . . . . . . . . . . 13
                                              |
19 | | eqid 2451 |
. . . . . . . . . . . . . 14
    
      
   |
20 | | eqid 2451 |
. . . . . . . . . . . . . 14
                   |
21 | 19, 20 | fvmptex 5960 |
. . . . . . . . . . . . 13
                         |
22 | | eqid 2451 |
. . . . . . . . . . . . . 14
    
      
   |
23 | | eqid 2451 |
. . . . . . . . . . . . . 14
                   |
24 | 22, 23 | fvmptex 5960 |
. . . . . . . . . . . . 13
                         |
25 | 18, 21, 24 | 3eqtr4g 2510 |
. . . . . . . . . . . 12
                       
          
       |
26 | 2, 25 | seqfeq 12238 |
. . . . . . . . . . 11
  
        
                      |
27 | 26 | breq1d 4412 |
. . . . . . . . . 10
  
        
         
             |
28 | 27 | anbi2d 710 |
. . . . . . . . 9
  
        
            

              |
29 | 28 | exbidv 1768 |
. . . . . . . 8
  
        
                                |
30 | 29 | rexbidva 2898 |
. . . . . . 7
 
   
 
                  
                       |
31 | 30 | adantr 467 |
. . . . . 6
  
      
                   
                      |
32 | | simpr 463 |
. . . . . . . 8
  
       |
33 | 15 | adantr 467 |
. . . . . . . . . . 11
  
        
              
     |
34 | 33 | fveq1d 5867 |
. . . . . . . . . 10
  
        
      
            
        |
35 | 34, 21, 24 | 3eqtr4g 2510 |
. . . . . . . . 9
  
        
                
       |
36 | 35 | adantlr 721 |
. . . . . . . 8
                   
          
       |
37 | 32, 36 | seqfeq 12238 |
. . . . . . 7
  
                           |
38 | 37 | breq1d 4412 |
. . . . . 6
  
              
             |
39 | 31, 38 | 3anbi23d 1342 |
. . . . 5
  
                                                                                 |
40 | 39 | rexbidva 2898 |
. . . 4
 
   
 
    
                          
    

    
                                 |
41 | | simplr 762 |
. . . . . . . . . 10
                 
  |
42 | | nnuz 11194 |
. . . . . . . . . 10
     |
43 | 41, 42 | syl6eleq 2539 |
. . . . . . . . 9
                 
      |
44 | | f1of 5814 |
. . . . . . . . . . . . . 14
        
          |
45 | 44 | ad2antlr 733 |
. . . . . . . . . . . . 13
    
                             |
46 | | ffvelrn 6020 |
. . . . . . . . . . . . 13
              
      |
47 | 45, 46 | sylancom 673 |
. . . . . . . . . . . 12
    
                         |
48 | | simplll 768 |
. . . . . . . . . . . 12
    
                   
      |
49 | | nfcsb1v 3379 |
. . . . . . . . . . . . . 14
        ![]_ ]_](_urbrack.gif)
   |
50 | | nfcsb1v 3379 |
. . . . . . . . . . . . . 14
        ![]_ ]_](_urbrack.gif)
   |
51 | 49, 50 | nfeq 2603 |
. . . . . . . . . . . . 13
        ![]_ ]_](_urbrack.gif)
        ![]_ ]_](_urbrack.gif)    |
52 | | csbeq1a 3372 |
. . . . . . . . . . . . . 14
             ![]_ ]_](_urbrack.gif)
    |
53 | | csbeq1a 3372 |
. . . . . . . . . . . . . 14
             ![]_ ]_](_urbrack.gif)
    |
54 | 52, 53 | eqeq12d 2466 |
. . . . . . . . . . . . 13
         
      ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
     |
55 | 51, 54 | rspc 3144 |
. . . . . . . . . . . 12
      
          ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
     |
56 | 47, 48, 55 | sylc 62 |
. . . . . . . . . . 11
    
                         ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)
    |
57 | | fvex 5875 |
. . . . . . . . . . . 12
     |
58 | | csbfv2g 5901 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)   |
60 | | csbfv2g 5901 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    |
61 | 57, 60 | ax-mp 5 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)   |
62 | 56, 59, 61 | 3eqtr3g 2508 |
. . . . . . . . . 10
    
                          ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)    |
63 | | elfznn 11828 |
. . . . . . . . . . . 12
       |
64 | 63 | adantl 468 |
. . . . . . . . . . 11
    
                     |
65 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
66 | 65 | csbeq1d 3370 |
. . . . . . . . . . . 12
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
67 | | eqid 2451 |
. . . . . . . . . . . 12
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
68 | 66, 67 | fvmpti 5947 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    |
69 | 64, 68 | syl 17 |
. . . . . . . . . 10
    
                           ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    |
70 | 65 | csbeq1d 3370 |
. . . . . . . . . . . 12
       ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
71 | | eqid 2451 |
. . . . . . . . . . . 12
       ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
72 | 70, 71 | fvmpti 5947 |
. . . . . . . . . . 11
         ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    |
73 | 64, 72 | syl 17 |
. . . . . . . . . 10
    
                           ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)    |
74 | 62, 69, 73 | 3eqtr4d 2495 |
. . . . . . . . 9
    
                           ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)       |
75 | 43, 74 | seqfveq 12237 |
. . . . . . . 8
                 
         ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)        |
76 | 75 | eqeq2d 2461 |
. . . . . . 7
                 

         ![]_ ]_](_urbrack.gif)     
         ![]_ ]_](_urbrack.gif)         |
77 | 76 | pm5.32da 647 |
. . . . . 6
  
                        ![]_ ]_](_urbrack.gif)      
                  ![]_ ]_](_urbrack.gif)          |
78 | 77 | exbidv 1768 |
. . . . 5
  
                          ![]_ ]_](_urbrack.gif)      
                    ![]_ ]_](_urbrack.gif)          |
79 | 78 | rexbidva 2898 |
. . . 4
 
   
 
                    ![]_ ]_](_urbrack.gif)      
           
         ![]_ ]_](_urbrack.gif)          |
80 | 40, 79 | orbi12d 716 |
. . 3
 
   
  

    
                                         
         ![]_ ]_](_urbrack.gif)                                         
               
         ![]_ ]_](_urbrack.gif)           |
81 | 80 | iotabidv 5567 |
. 2
 
   
                                    
               
         ![]_ ]_](_urbrack.gif)                                             
               
         ![]_ ]_](_urbrack.gif)           |
82 | | df-prod 13960 |
. 2

         
                          
               
         ![]_ ]_](_urbrack.gif)          |
83 | | df-prod 13960 |
. 2

         
                          
               
         ![]_ ]_](_urbrack.gif)          |
84 | 81, 82, 83 | 3eqtr4g 2510 |
1
 
   
    |