Step | Hyp | Ref
| Expression |
1 | | tailfb.1 |
. . . . 5
 |
2 | 1 | tailf 31102 |
. . . 4
            |
3 | | frn 5747 |
. . . 4
             
   |
4 | 2, 3 | syl 17 |
. . 3

       |
5 | 4 | adantr 472 |
. 2
          |
6 | | n0 3732 |
. . . . 5
    |
7 | | ffn 5739 |
. . . . . . . 8
                |
8 | | fnfvelrn 6034 |
. . . . . . . . 9
     
               |
9 | 8 | ex 441 |
. . . . . . . 8
    
                |
10 | 2, 7, 9 | 3syl 18 |
. . . . . . 7
 
               |
11 | | ne0i 3728 |
. . . . . . 7
            
      |
12 | 10, 11 | syl6 33 |
. . . . . 6
 
       |
13 | 12 | exlimdv 1787 |
. . . . 5
  
       |
14 | 6, 13 | syl5bi 225 |
. . . 4
 
       |
15 | 14 | imp 436 |
. . 3
         |
16 | 1 | tailini 31103 |
. . . . . . . 8
             |
17 | | n0i 3727 |
. . . . . . . 8
        
          |
18 | 16, 17 | syl 17 |
. . . . . . 7
             |
19 | 18 | nrexdv 2842 |
. . . . . 6


          |
20 | 19 | adantr 472 |
. . . . 5
              |
21 | | fvelrnb 5926 |
. . . . . . 7
    
                 |
22 | 2, 7, 21 | 3syl 18 |
. . . . . 6
                  |
23 | 22 | adantr 472 |
. . . . 5
   
   

           |
24 | 20, 23 | mtbird 308 |
. . . 4
  
      |
25 | | df-nel 2644 |
. . . 4
    
      |
26 | 24, 25 | sylibr 217 |
. . 3
         |
27 | | fvelrnb 5926 |
. . . . . . . 8
    
    

           |
28 | | fvelrnb 5926 |
. . . . . . . 8
    
    

           |
29 | 27, 28 | anbi12d 725 |
. . . . . . 7
    
     
    
 
                     |
30 | 2, 7, 29 | 3syl 18 |
. . . . . 6
           
 
                     |
31 | | reeanv 2944 |
. . . . . . 7
  
        
          
                    |
32 | 1 | dirge 16561 |
. . . . . . . . . . 11
 
 
  
     |
33 | 32 | 3expb 1232 |
. . . . . . . . . 10
  
 

  
     |
34 | 2, 7 | syl 17 |
. . . . . . . . . . . . 13
       |
35 | | fnfvelrn 6034 |
. . . . . . . . . . . . 13
     
               |
36 | 34, 35 | sylan 479 |
. . . . . . . . . . . 12
                 |
37 | 36 | ad2ant2r 761 |
. . . . . . . . . . 11
   
                         |
38 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
39 | | dirtr 16560 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
40 | 39 | exp32 616 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
41 | 38, 40 | mpan2 685 |
. . . . . . . . . . . . . . . . . . . . 21
   
  
      |
42 | 41 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
   
  
      |
43 | 42 | imp 436 |
. . . . . . . . . . . . . . . . . . 19
             |
44 | 43 | ad2ant2rl 763 |
. . . . . . . . . . . . . . . . . 18
   
         
     |
45 | | dirtr 16560 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
46 | 45 | exp32 616 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
47 | 38, 46 | mpan2 685 |
. . . . . . . . . . . . . . . . . . . . 21
   
  
      |
48 | 47 | com23 80 |
. . . . . . . . . . . . . . . . . . . 20
   
  
      |
49 | 48 | imp 436 |
. . . . . . . . . . . . . . . . . . 19
             |
50 | 49 | ad2ant2rl 763 |
. . . . . . . . . . . . . . . . . 18
   
         
     |
51 | 44, 50 | anim12d 572 |
. . . . . . . . . . . . . . . . 17
   
                       |
52 | 51 | expr 626 |
. . . . . . . . . . . . . . . 16
   
                       |
53 | 52 | com23 80 |
. . . . . . . . . . . . . . 15
   
         
  
          |
54 | 53 | impr 631 |
. . . . . . . . . . . . . 14
   
                       |
55 | 1 | eltail 31101 |
. . . . . . . . . . . . . . . 16
 
         
     |
56 | 38, 55 | mp3an3 1379 |
. . . . . . . . . . . . . . 15
           
     |
57 | 56 | ad2ant2r 761 |
. . . . . . . . . . . . . 14
   
                         |
58 | 1 | eltail 31101 |
. . . . . . . . . . . . . . . . . 18
 
         
     |
59 | 38, 58 | mp3an3 1379 |
. . . . . . . . . . . . . . . . 17
           
     |
60 | 59 | adantrr 731 |
. . . . . . . . . . . . . . . 16
  
 
              |
61 | 1 | eltail 31101 |
. . . . . . . . . . . . . . . . . 18
 
         
     |
62 | 38, 61 | mp3an3 1379 |
. . . . . . . . . . . . . . . . 17
           
     |
63 | 62 | adantrl 730 |
. . . . . . . . . . . . . . . 16
  
 
              |
64 | 60, 63 | anbi12d 725 |
. . . . . . . . . . . . . . 15
  
 
                            |
65 | 64 | adantr 472 |
. . . . . . . . . . . . . 14
   
                    
        
  
      |
66 | 54, 57, 65 | 3imtr4d 276 |
. . . . . . . . . . . . 13
   
                            
            |
67 | | elin 3608 |
. . . . . . . . . . . . 13
                  
        
           |
68 | 66, 67 | syl6ibr 235 |
. . . . . . . . . . . 12
   
                                         |
69 | 68 | ssrdv 3424 |
. . . . . . . . . . 11
   
                           
           |
70 | | sseq1 3439 |
. . . . . . . . . . . 12
        
         
        
                             |
71 | 70 | rspcev 3136 |
. . . . . . . . . . 11
             
                                                     |
72 | 37, 69, 71 | syl2anc 673 |
. . . . . . . . . 10
   
           
    
                    |
73 | 33, 72 | rexlimddv 2875 |
. . . . . . . . 9
  
 
                          |
74 | | ineq1 3618 |
. . . . . . . . . . . 12
        
                              |
75 | 74 | sseq2d 3446 |
. . . . . . . . . . 11
        
                  

            |
76 | 75 | rexbidv 2892 |
. . . . . . . . . 10
        
                        
      
            |
77 | | ineq2 3619 |
. . . . . . . . . . . 12
        
              |
78 | 77 | sseq2d 3446 |
. . . . . . . . . . 11
        
           
    |
79 | 78 | rexbidv 2892 |
. . . . . . . . . 10
        
                      
     |
80 | 76, 79 | sylan9bb 714 |
. . . . . . . . 9
         
        
 
             
        
      
    |
81 | 73, 80 | syl5ibcom 228 |
. . . . . . . 8
  
 
         
        
      
    |
82 | 81 | rexlimdvva 2878 |
. . . . . . 7
  

                       
     |
83 | 31, 82 | syl5bir 226 |
. . . . . 6
           

        
      
    |
84 | 30, 83 | sylbid 223 |
. . . . 5
                  
    |
85 | 84 | adantr 472 |
. . . 4
        
    
      
    |
86 | 85 | ralrimivv 2813 |
. . 3
                     
   |
87 | 15, 26, 86 | 3jca 1210 |
. 2
                  
     
    
     |
88 | | dmexg 6743 |
. . . . 5

  |
89 | 1, 88 | syl5eqel 2553 |
. . . 4
   |
90 | 89 | adantr 472 |
. . 3
     |
91 | | isfbas2 20928 |
. . 3
         
                     
     
    
       |
92 | 90, 91 | syl 17 |
. 2
           
                     
     
    
       |
93 | 5, 87, 92 | mpbir2and 936 |
1
             |