Step | Hyp | Ref
| Expression |
1 | | simprl 764 |
. . . . 5
  

    


               
      |
2 | | fof 5793 |
. . . . 5
           |
3 | 1, 2 | syl 17 |
. . . 4
  

    


               
      |
4 | | simpll 760 |
. . . . . . . 8
  

    


               
  |
5 | | sotrieq 4782 |
. . . . . . . . 9
  
  
         |
6 | 5 | con2bid 331 |
. . . . . . . 8
  
        
   |
7 | 4, 6 | sylan 474 |
. . . . . . 7
    
    


                         
   |
8 | | simprr 766 |
. . . . . . . . . 10
  

    


               


                |
9 | | breq1 4405 |
. . . . . . . . . . . . 13
   
     |
10 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
11 | 10 | breq1d 4412 |
. . . . . . . . . . . . 13
           
             |
12 | 9, 11 | imbi12d 322 |
. . . . . . . . . . . 12
                  
              |
13 | | breq2 4406 |
. . . . . . . . . . . . 13
   
     |
14 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
15 | 14 | breq2d 4414 |
. . . . . . . . . . . . 13
           
             |
16 | 13, 15 | imbi12d 322 |
. . . . . . . . . . . 12
                  
              |
17 | 12, 16 | rspc2va 3160 |
. . . . . . . . . . 11
  



                 
             |
18 | 17 | ancoms 455 |
. . . . . . . . . 10
   
                                 |
19 | 8, 18 | sylan 474 |
. . . . . . . . 9
    
    


                                   |
20 | | simpllr 769 |
. . . . . . . . . . 11
    
    


                  
  |
21 | | simplrl 770 |
. . . . . . . . . . . . 13
    
    


                         |
22 | 21, 2 | syl 17 |
. . . . . . . . . . . 12
    
    


                         |
23 | | simprr 766 |
. . . . . . . . . . . 12
    
    


                     |
24 | 22, 23 | ffvelrnd 6023 |
. . . . . . . . . . 11
    
    


                         |
25 | | poirr 4766 |
. . . . . . . . . . . 12
                   |
26 | | breq1 4405 |
. . . . . . . . . . . . 13
                   
             |
27 | 26 | notbid 296 |
. . . . . . . . . . . 12
                   
             |
28 | 25, 27 | syl5ibrcom 226 |
. . . . . . . . . . 11
               
             |
29 | 20, 24, 28 | syl2anc 667 |
. . . . . . . . . 10
    
    


                           
             |
30 | 29 | con2d 119 |
. . . . . . . . 9
    
    


                             
           |
31 | 19, 30 | syld 45 |
. . . . . . . 8
    
    


                     
           |
32 | | breq1 4405 |
. . . . . . . . . . . . . 14
   
     |
33 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
34 | 33 | breq1d 4412 |
. . . . . . . . . . . . . 14
           
             |
35 | 32, 34 | imbi12d 322 |
. . . . . . . . . . . . 13
                  
              |
36 | | breq2 4406 |
. . . . . . . . . . . . . 14
   
     |
37 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
38 | 37 | breq2d 4414 |
. . . . . . . . . . . . . 14
           
             |
39 | 36, 38 | imbi12d 322 |
. . . . . . . . . . . . 13
                  
              |
40 | 35, 39 | rspc2va 3160 |
. . . . . . . . . . . 12
  



                 
             |
41 | 40 | ancoms 455 |
. . . . . . . . . . 11
   
                                 |
42 | 41 | ancom2s 811 |
. . . . . . . . . 10
   
                                 |
43 | 8, 42 | sylan 474 |
. . . . . . . . 9
    
    


                                   |
44 | | breq2 4406 |
. . . . . . . . . . . . 13
                   
             |
45 | 44 | notbid 296 |
. . . . . . . . . . . 12
                   
             |
46 | 25, 45 | syl5ibrcom 226 |
. . . . . . . . . . 11
               
             |
47 | 20, 24, 46 | syl2anc 667 |
. . . . . . . . . 10
    
    


                           
             |
48 | 47 | con2d 119 |
. . . . . . . . 9
    
    


                             
           |
49 | 43, 48 | syld 45 |
. . . . . . . 8
    
    


                     
           |
50 | 31, 49 | jaod 382 |
. . . . . . 7
    
    


                                     |
51 | 7, 50 | sylbird 239 |
. . . . . 6
    
    


                   
           |
52 | 51 | con4d 109 |
. . . . 5
    
    


                               |
53 | 52 | ralrimivva 2809 |
. . . 4
  

    


               


            |
54 | | dff13 6159 |
. . . 4
    
     

             |
55 | 3, 53, 54 | sylanbrc 670 |
. . 3
  

    


               
      |
56 | | df-f1o 5589 |
. . 3
         
       |
57 | 55, 1, 56 | sylanbrc 670 |
. 2
  

    


               
      |
58 | | sotric 4781 |
. . . . . . 7
  
    
       |
59 | 58 | con2bid 331 |
. . . . . 6
  
      
     |
60 | 4, 59 | sylan 474 |
. . . . 5
    
    


                       
     |
61 | | fveq2 5865 |
. . . . . . . . . 10
           |
62 | 61 | breq1d 4412 |
. . . . . . . . 9
           
             |
63 | 62 | notbid 296 |
. . . . . . . 8
           
             |
64 | 25, 63 | syl5ibrcom 226 |
. . . . . . 7
       
             |
65 | 20, 24, 64 | syl2anc 667 |
. . . . . 6
    
    


                   
             |
66 | | simprl 764 |
. . . . . . . . 9
    
    


                     |
67 | 22, 66 | ffvelrnd 6023 |
. . . . . . . 8
    
    


                         |
68 | | po2nr 4768 |
. . . . . . . . 9
            
                        |
69 | | imnan 424 |
. . . . . . . . 9
                                               |
70 | 68, 69 | sylibr 216 |
. . . . . . . 8
            
                        |
71 | 20, 24, 67, 70 | syl12anc 1266 |
. . . . . . 7
    
    


                             
             |
72 | 43, 71 | syld 45 |
. . . . . 6
    
    


                     
             |
73 | 65, 72 | jaod 382 |
. . . . 5
    
    


                                     |
74 | 60, 73 | sylbird 239 |
. . . 4
    
    


                     
             |
75 | 19, 74 | impcon4bid 209 |
. . 3
    
    


                                   |
76 | 75 | ralrimivva 2809 |
. 2
  

    


               


  
             |
77 | | df-isom 5591 |
. 2
           
                 |
78 | 57, 76, 77 | sylanbrc 670 |
1
  

    


               
      |