Step | Hyp | Ref
| Expression |
1 | | f1ofo 5843 |
. . . 4
    
      |
2 | | df-fo 5606 |
. . . . 5
    

   |
3 | | freq2 4823 |
. . . . . . 7
     |
4 | 3 | biimprd 231 |
. . . . . 6
     |
5 | | df-fn 5603 |
. . . . . . 7

    |
6 | | df-fr 4811 |
. . . . . . . . . . . . . . . . . . . 20

    


     |
7 | | vex 3059 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
8 | 7 | funimaex 5682 |
. . . . . . . . . . . . . . . . . . . . 21

      |
9 | | n0 3752 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    |
10 | | funfvima2 6165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
11 | | ne0i 3748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
12 | 10, 11 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
13 | 12 | exlimdv 1789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
14 | 9, 13 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
15 | 14 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
16 | | imassrn 5197 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
17 | 15, 16 | jctil 544 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
18 | | sseq1 3464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
19 | | neeq1 2697 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
20 | 18, 19 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
             |
21 | | raleq 2998 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
 
          |
22 | 21 | rexeqbi1dv 3007 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      

 
                |
23 | 20, 22 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . 23
        


  
     
                      |
24 | 23 | spcgv 3145 |
. . . . . . . . . . . . . . . . . . . . . 22
         
 

             
                 |
25 | 17, 24 | syl7 70 |
. . . . . . . . . . . . . . . . . . . . 21
         
 

     
                   |
26 | 8, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20

    
 

     
                   |
27 | 6, 26 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . 19

   


                 |
28 | 27 | com23 81 |
. . . . . . . . . . . . . . . . . 18

  
                    |
29 | 28 | expd 442 |
. . . . . . . . . . . . . . . . 17

    

     
           |
30 | 29 | anabsi5 831 |
. . . . . . . . . . . . . . . 16
    

     
          |
31 | 30 | impd 437 |
. . . . . . . . . . . . . . 15
     
                |
32 | | fores 5824 |
. . . . . . . . . . . . . . . 16
               |
33 | | fvres 5901 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
34 | | fvres 5901 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
35 | 33, 34 | breqan12rd 4432 |
. . . . . . . . . . . . . . . . . . . . 21
 
           
   
             |
36 | | vex 3059 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
37 | | vex 3059 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
38 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
39 | 38 | breq1d 4425 |
. . . . . . . . . . . . . . . . . . . . . 22
           
             |
40 | | fveq2 5887 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
41 | 40 | breq2d 4427 |
. . . . . . . . . . . . . . . . . . . . . 22
           
             |
42 | | f1oweALT.1 |
. . . . . . . . . . . . . . . . . . . . . 22
   
            |
43 | 36, 37, 39, 41, 42 | brab 4737 |
. . . . . . . . . . . . . . . . . . . . 21
  
            |
44 | 35, 43 | syl6rbbr 272 |
. . . . . . . . . . . . . . . . . . . 20
 
             
       |
45 | 44 | notbid 300 |
. . . . . . . . . . . . . . . . . . 19
 
   
                 |
46 | 45 | ralbidva 2835 |
. . . . . . . . . . . . . . . . . 18
  
 

                 |
47 | 46 | rexbiia 2899 |
. . . . . . . . . . . . . . . . 17
  
 


                |
48 | | breq1 4418 |
. . . . . . . . . . . . . . . . . . . . 21
      
                          |
49 | 48 | notbid 300 |
. . . . . . . . . . . . . . . . . . . 20
      
          
   
           |
50 | 49 | cbvfo 6211 |
. . . . . . . . . . . . . . . . . . 19
 
            
                    
       |
51 | 50 | rexbidv 2912 |
. . . . . . . . . . . . . . . . . 18
 
             
             
               |
52 | | breq2 4419 |
. . . . . . . . . . . . . . . . . . . . 21
      
              |
53 | 52 | notbid 300 |
. . . . . . . . . . . . . . . . . . . 20
      
    
   
     |
54 | 53 | ralbidv 2838 |
. . . . . . . . . . . . . . . . . . 19
      
 
                      |
55 | 54 | cbvexfo 6212 |
. . . . . . . . . . . . . . . . . 18
 
                                        |
56 | 51, 55 | bitrd 261 |
. . . . . . . . . . . . . . . . 17
 
             
                  
         |
57 | 47, 56 | syl5bb 265 |
. . . . . . . . . . . . . . . 16
 
                              |
58 | 32, 57 | syl 17 |
. . . . . . . . . . . . . . 15
                        |
59 | 31, 58 | sylibrd 242 |
. . . . . . . . . . . . . 14
     


     |
60 | 59 | exp4b 616 |
. . . . . . . . . . . . 13



 

       |
61 | 60 | com34 86 |
. . . . . . . . . . . 12


  

       |
62 | 61 | com23 81 |
. . . . . . . . . . 11

 
 

       |
63 | 62 | imp4a 598 |
. . . . . . . . . 10

    

      |
64 | 63 | alrimdv 1785 |
. . . . . . . . 9

     


      |
65 | | df-fr 4811 |
. . . . . . . . 9

    


     |
66 | 64, 65 | syl6ibr 235 |
. . . . . . . 8

    |
67 | | freq2 4823 |
. . . . . . . . 9
     |
68 | 67 | biimpd 212 |
. . . . . . . 8
     |
69 | 66, 68 | sylan9 667 |
. . . . . . 7
       |
70 | 5, 69 | sylbi 200 |
. . . . . 6
 
   |
71 | 4, 70 | sylan9r 668 |
. . . . 5
       |
72 | 2, 71 | sylbi 200 |
. . . 4
         |
73 | 1, 72 | syl 17 |
. . 3
    

   |
74 | | df-f1o 5607 |
. . . . 5
         
       |
75 | | fveq2 5887 |
. . . . . . . . . . 11
           |
76 | 75 | breq1d 4425 |
. . . . . . . . . 10
           
             |
77 | | fveq2 5887 |
. . . . . . . . . . 11
           |
78 | 77 | breq2d 4427 |
. . . . . . . . . 10
           
             |
79 | 37, 36, 76, 78, 42 | brab 4737 |
. . . . . . . . 9
  
            |
80 | 79 | a1i 11 |
. . . . . . . 8
      
    
             |
81 | | f1fveq 6187 |
. . . . . . . . 9
      
          
   |
82 | 81 | bicomd 206 |
. . . . . . . 8
      
  
           |
83 | 43 | a1i 11 |
. . . . . . . 8
      
    
             |
84 | 80, 82, 83 | 3orbi123d 1347 |
. . . . . . 7
      
                                          |
85 | 84 | 2ralbidva 2841 |
. . . . . 6
             


                                 |
86 | | breq1 4418 |
. . . . . . . . . 10
               
         |
87 | | eqeq1 2465 |
. . . . . . . . . 10
             
       |
88 | | breq2 4419 |
. . . . . . . . . 10
               
         |
89 | 86, 87, 88 | 3orbi123d 1347 |
. . . . . . . . 9
                                                         |
90 | 89 | ralbidv 2838 |
. . . . . . . 8
      
                                                    |
91 | 90 | cbvfo 6211 |
. . . . . . 7
                                     


                     |
92 | | breq2 4419 |
. . . . . . . . . 10
           
     |
93 | | eqeq2 2472 |
. . . . . . . . . 10
         
   |
94 | | breq1 4418 |
. . . . . . . . . 10
           
     |
95 | 92, 93, 94 | 3orbi123d 1347 |
. . . . . . . . 9
                                 |
96 | 95 | cbvfo 6211 |
. . . . . . . 8
                        

  
      |
97 | 96 | ralbidv 2838 |
. . . . . . 7
                         


  
      |
98 | 91, 97 | bitrd 261 |
. . . . . 6
                                     


  
      |
99 | 85, 98 | sylan9bb 711 |
. . . . 5
          
 

      

         |
100 | 74, 99 | sylbi 200 |
. . . 4
    
 

      

         |
101 | 100 | biimprd 231 |
. . 3
    
 

       
         |
102 | 73, 101 | anim12d 570 |
. 2
    
 
 
      



  
       |
103 | | dfwe2 6634 |
. 2




  
      |
104 | | dfwe2 6634 |
. 2




  
      |
105 | 102, 103,
104 | 3imtr4g 278 |
1
    

   |