Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. . 3
   |
2 | | flift.1 |
. . . . 5
      |
3 | | nfmpt1 3841 |
. . . . . 6
  
     |
4 | 3 | nfrn 4522 |
. . . . 5
        |
5 | 2, 4 | nfcxfr 2172 |
. . . 4
   |
6 | 5 | nffun 4867 |
. . 3
   |
7 | | fveq2 5121 |
. . . . . . 7
           |
8 | | simplr 482 |
. . . . . . . . 9
         |
9 | | flift.2 |
. . . . . . . . . . 11
     |
10 | | flift.3 |
. . . . . . . . . . 11
     |
11 | 2, 9, 10 | fliftel1 5377 |
. . . . . . . . . 10
       |
12 | 11 | ad2ant2r 478 |
. . . . . . . . 9
           |
13 | | funbrfv 5155 |
. . . . . . . . 9

  
       |
14 | 8, 12, 13 | sylc 56 |
. . . . . . . 8
             |
15 | | simprr 484 |
. . . . . . . . . . 11
      
  |
16 | | eqidd 2038 |
. . . . . . . . . . 11
         |
17 | | eqidd 2038 |
. . . . . . . . . . 11
         |
18 | | fliftfun.4 |
. . . . . . . . . . . . . 14
   |
19 | 18 | eqeq2d 2048 |
. . . . . . . . . . . . 13
 
   |
20 | | fliftfun.5 |
. . . . . . . . . . . . . 14
   |
21 | 20 | eqeq2d 2048 |
. . . . . . . . . . . . 13
 
   |
22 | 19, 21 | anbi12d 442 |
. . . . . . . . . . . 12
  
 
    |
23 | 22 | rspcev 2650 |
. . . . . . . . . . 11
  
 


   |
24 | 15, 16, 17, 23 | syl12anc 1132 |
. . . . . . . . . 10
       

   |
25 | 2, 9, 10 | fliftel 5376 |
. . . . . . . . . . 11
     
    |
26 | 25 | ad2antrr 457 |
. . . . . . . . . 10
          

    |
27 | 24, 26 | mpbird 156 |
. . . . . . . . 9
           |
28 | | funbrfv 5155 |
. . . . . . . . 9

  
       |
29 | 8, 27, 28 | sylc 56 |
. . . . . . . 8
             |
30 | 14, 29 | eqeq12d 2051 |
. . . . . . 7
           
       |
31 | 7, 30 | syl5ib 143 |
. . . . . 6
       
   |
32 | 31 | anassrs 380 |
. . . . 5
       
   |
33 | 32 | ralrimiva 2386 |
. . . 4
     

   |
34 | 33 | exp31 346 |
. . 3
  
 
     |
35 | 1, 6, 34 | ralrimd 2391 |
. 2
  


    |
36 | 2, 9, 10 | fliftel 5376 |
. . . . . . . . 9
     
    |
37 | 2, 9, 10 | fliftel 5376 |
. . . . . . . . . 10
     
    |
38 | 18 | eqeq2d 2048 |
. . . . . . . . . . . 12
 
   |
39 | 20 | eqeq2d 2048 |
. . . . . . . . . . . 12
 
   |
40 | 38, 39 | anbi12d 442 |
. . . . . . . . . . 11
  
 
    |
41 | 40 | cbvrexv 2528 |
. . . . . . . . . 10
 

 

   |
42 | 37, 41 | syl6bb 185 |
. . . . . . . . 9
     
    |
43 | 36, 42 | anbi12d 442 |
. . . . . . . 8
         

  
     |
44 | 43 | biimpd 132 |
. . . . . . 7
         

        |
45 | | reeanv 2473 |
. . . . . . . 8
 

 
     

  
    |
46 | | r19.29 2444 |
. . . . . . . . . 10
  


  
 
        
   
       |
47 | | r19.29 2444 |
. . . . . . . . . . . 12
  

   
            
     |
48 | | eqtr2 2055 |
. . . . . . . . . . . . . . . . 17
 
   |
49 | 48 | ad2ant2r 478 |
. . . . . . . . . . . . . . . 16
  
   
  |
50 | 49 | imim1i 54 |
. . . . . . . . . . . . . . 15
 
     
     |
51 | 50 | imp 115 |
. . . . . . . . . . . . . 14
       
  
  |
52 | | simprlr 490 |
. . . . . . . . . . . . . 14
       
  
  |
53 | | simprrr 492 |
. . . . . . . . . . . . . 14
       
  
  |
54 | 51, 52, 53 | 3eqtr4d 2079 |
. . . . . . . . . . . . 13
       
  
  |
55 | 54 | rexlimivw 2423 |
. . . . . . . . . . . 12
 
 
    
  
  |
56 | 47, 55 | syl 14 |
. . . . . . . . . . 11
  

   
       |
57 | 56 | rexlimivw 2423 |
. . . . . . . . . 10
 
 

   
       |
58 | 46, 57 | syl 14 |
. . . . . . . . 9
  


  
 
       |
59 | 58 | ex 108 |
. . . . . . . 8
 


   
 
   
   |
60 | 45, 59 | syl5bir 142 |
. . . . . . 7
 


      

     |
61 | 44, 60 | syl9 66 |
. . . . . 6
            
    |
62 | 61 | alrimdv 1753 |
. . . . 5
                   |
63 | 62 | alrimdv 1753 |
. . . 4
                     |
64 | 63 | alrimdv 1753 |
. . 3
                  
    |
65 | 2, 9, 10 | fliftrel 5375 |
. . . . 5

    |
66 | | relxp 4390 |
. . . . 5
   |
67 | | relss 4370 |
. . . . 5
  
      |
68 | 65, 66, 67 | mpisyl 1332 |
. . . 4
   |
69 | | dffun2 4855 |
. . . . 5
                   |
70 | 69 | baib 827 |
. . . 4

                  |
71 | 68, 70 | syl 14 |
. . 3
                   |
72 | 64, 71 | sylibrd 158 |
. 2
         |
73 | 35, 72 | impbid 120 |
1
  


    |