Step | Hyp | Ref
| Expression |
1 | | simpl 464 |
. 2
     
   


                      |
2 | | f1of1 5827 |
. . 3
    
      |
3 | | df-br 4396 |
. . . . 5
          
             |
4 | | eleq2 2538 |
. . . . . . 7
    


                          
              


                  |
5 | | fvex 5889 |
. . . . . . . . 9
     |
6 | | fvex 5889 |
. . . . . . . . 9
     |
7 | | eqeq1 2475 |
. . . . . . . . . . . 12
         
           |
8 | 7 | anbi1d 719 |
. . . . . . . . . . 11
                        
        |
9 | 8 | anbi1d 719 |
. . . . . . . . . 10
           
       
         
           |
10 | 9 | 2rexbidv 2897 |
. . . . . . . . 9
      

     
       


         
           |
11 | | eqeq1 2475 |
. . . . . . . . . . . 12
         
           |
12 | 11 | anbi2d 718 |
. . . . . . . . . . 11
                            
            |
13 | 12 | anbi1d 719 |
. . . . . . . . . 10
               
       
                         |
14 | 13 | 2rexbidv 2897 |
. . . . . . . . 9
      

         
       


                         |
15 | 5, 6, 10, 14 | opelopab 4723 |
. . . . . . . 8
                                 

         
              |
16 | | anass 661 |
. . . . . . . . . . . . . . 15
                      
                        |
17 | | f1fveq 6181 |
. . . . . . . . . . . . . . . . . 18
      
          
   |
18 | | equcom 1870 |
. . . . . . . . . . . . . . . . . 18

  |
19 | 17, 18 | syl6bb 269 |
. . . . . . . . . . . . . . . . 17
      
          
   |
20 | 19 | anassrs 660 |
. . . . . . . . . . . . . . . 16
       
         
   |
21 | 20 | anbi1d 719 |
. . . . . . . . . . . . . . 15
       
                   
   

                |
22 | 16, 21 | syl5bb 265 |
. . . . . . . . . . . . . 14
       
           
           

                |
23 | 22 | rexbidv 2892 |
. . . . . . . . . . . . 13
       
  
         
           


                |
24 | | r19.42v 2931 |
. . . . . . . . . . . . 13
               


               |
25 | 23, 24 | syl6bb 269 |
. . . . . . . . . . . 12
       
  
         
           


                |
26 | 25 | rexbidva 2889 |
. . . . . . . . . . 11
     

 

                     



                |
27 | | breq1 4398 |
. . . . . . . . . . . . . . 15
   
     |
28 | 27 | anbi2d 718 |
. . . . . . . . . . . . . 14
                      
      |
29 | 28 | rexbidv 2892 |
. . . . . . . . . . . . 13
  
                            |
30 | 29 | ceqsrexv 3160 |
. . . . . . . . . . . 12
  

             

               |
31 | 30 | adantl 473 |
. . . . . . . . . . 11
     

 
               
               |
32 | 26, 31 | bitrd 261 |
. . . . . . . . . 10
     

 

                     

               |
33 | | f1fveq 6181 |
. . . . . . . . . . . . . . 15
      
          
   |
34 | | equcom 1870 |
. . . . . . . . . . . . . . 15

  |
35 | 33, 34 | syl6bb 269 |
. . . . . . . . . . . . . 14
      
          
   |
36 | 35 | anassrs 660 |
. . . . . . . . . . . . 13
       
         
   |
37 | 36 | anbi1d 719 |
. . . . . . . . . . . 12
       
                     |
38 | 37 | rexbidva 2889 |
. . . . . . . . . . 11
     

 
           


      |
39 | | breq2 4399 |
. . . . . . . . . . . . 13
   
     |
40 | 39 | ceqsrexv 3160 |
. . . . . . . . . . . 12
  
         |
41 | 40 | adantl 473 |
. . . . . . . . . . 11
     

 
   
     |
42 | 38, 41 | bitrd 261 |
. . . . . . . . . 10
     

 
           
     |
43 | 32, 42 | sylan9bb 714 |
. . . . . . . . 9
       
    
                          
     |
44 | 43 | anandis 846 |
. . . . . . . 8
      
   

         
           
     |
45 | 15, 44 | syl5bb 265 |
. . . . . . 7
      
                                        |
46 | 4, 45 | sylan9bbr 715 |
. . . . . 6
         
   


                                 |
47 | 46 | an32s 821 |
. . . . 5
            
     
                        
     |
48 | 3, 47 | syl5rbb 266 |
. . . 4
            
     
                             |
49 | 48 | ralrimivva 2814 |
. . 3
     
     
     
           
                |
50 | 2, 49 | sylan 479 |
. 2
     
   


                 
                |
51 | | df-isom 5598 |
. 2
           
                 |
52 | 1, 50, 51 | sylanbrc 677 |
1
     
   


                
     |