Step | Hyp | Ref
| Expression |
1 | | is2ndc 20538 |
. . 3

 
       |
2 | | omex 8166 |
. . . . . . 7
 |
3 | 2 | brdom 7599 |
. . . . . 6
        |
4 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . . . . 20
             |
5 | | f1f 5792 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
6 | | frn 5747 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
8 | 7 | adantl 473 |
. . . . . . . . . . . . . . . . . . . 20
         |
9 | 4, 8 | syl5ss 3429 |
. . . . . . . . . . . . . . . . . . 19
       
             |
10 | 9 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
        
         
              |
11 | | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . . 20
        
    
   |
12 | | n0 3732 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
13 | | tg2 20057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       

   |
14 | | omsson 6715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
15 | 9, 14 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
             |
16 | 15 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               
             |
17 | | f1fn 5793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
18 | 17 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 |
19 | | simprl 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                 |
20 | | fnfvelrn 6034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
       |
21 | 18, 19, 20 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     |
22 | | f1f1orn 5839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
23 | 22 | ad3antlr 745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                     |
24 | | f1ocnvfv1 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     

           |
25 | 23, 19, 24 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                          |
26 | | simprrr 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
              
  |
27 | | selpw 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
  |
28 | 26, 27 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                  |
29 | | simprrl 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                 |
30 | | ne0i 3728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                 |
32 | | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
     |
33 | 28, 31, 32 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                      |
34 | 25, 33 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                               |
35 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                     |
36 | 35 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
               
                 |
37 | 36 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     
             |
38 | 21, 34, 37 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               
             |
39 | | rabn0 3755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                           |
40 | 38, 39 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               
             |
41 | | onint 6641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
          
              
                         |
42 | 16, 40, 41 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                
                         |
43 | 42 | rexlimdvaa 2872 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       

 
   
                          |
44 | 13, 43 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       

 
                                 |
45 | 44 | expdimp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
              

                            |
46 | 45 | exlimdv 1787 |
. . . . . . . . . . . . . . . . . . . . . 22
              
 
                            |
47 | 12, 46 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . . . 21
              

                            |
48 | 47 | expimpd 614 |
. . . . . . . . . . . . . . . . . . . 20
       

 
                                 |
49 | 11, 48 | syl5bi 225 |
. . . . . . . . . . . . . . . . . . 19
       

     
                               |
50 | 49 | impr 631 |
. . . . . . . . . . . . . . . . . 18
        
         
                           |
51 | 10, 50 | sseldd 3419 |
. . . . . . . . . . . . . . . . 17
        
         
               |
52 | 51 | expr 626 |
. . . . . . . . . . . . . . . 16
       

     
                   |
53 | 52 | ralimdva 2805 |
. . . . . . . . . . . . . . 15
                 
 
              |
54 | 53 | imp 436 |
. . . . . . . . . . . . . 14
        
           
             |
55 | 54 | adantrr 731 |
. . . . . . . . . . . . 13
                       
               |
56 | | eqid 2471 |
. . . . . . . . . . . . . 14
                 
             |
57 | 56 | fmpt 6058 |
. . . . . . . . . . . . 13
 
            

                    |
58 | 55, 57 | sylib 201 |
. . . . . . . . . . . 12
                         
                  |
59 | | neeq1 2705 |
. . . . . . . . . . . . . . . . . . 19
                                             |
60 | | neeq1 2705 |
. . . . . . . . . . . . . . . . . . 19
                                   |
61 | | 1n0 7215 |
. . . . . . . . . . . . . . . . . . 19
 |
62 | 59, 60, 61 | elimhyp 3930 |
. . . . . . . . . . . . . . . . . 18
                |
63 | | n0 3732 |
. . . . . . . . . . . . . . . . . 18
               
                  |
64 | 62, 63 | mpbi 213 |
. . . . . . . . . . . . . . . . 17
                 |
65 | | 19.29r 1744 |
. . . . . . . . . . . . . . . . 17
                     
                  
   |
66 | 64, 65 | mpan 684 |
. . . . . . . . . . . . . . . 16
   
                  
   |
67 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                          
                            |
68 | 50, 67 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
        
         
              
              |
69 | 68 | imp 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         
           
           
              |
70 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
             |
71 | 70 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
           
             |
72 | 71 | elrab 3184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
            
              |
73 | 72 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                         |
74 | 69, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
           
           
            |
75 | | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                          |
76 | 74, 75 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
           
           
               |
77 | 76 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
           
           
       |
78 | 77 | iftrued 3880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
           
           
                      |
79 | 76 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         
           
           
        |
80 | 79 | elpwid 3952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
           
           
       |
81 | 78, 80 | eqsstrd 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
           
           
                 |
82 | 81 | sseld 3417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
           
           
                   |
83 | 82 | exp31 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
   
                                   |
84 | 83 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                           
   
                     |
85 | 84 | exp4a 617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     
     
                         |
86 | 85 | com25 93 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                     |
87 | 86 | imp31 439 |
. . . . . . . . . . . . . . . . . . . . . 22
                         
     
     
               |
88 | 87 | ralimdva 2805 |
. . . . . . . . . . . . . . . . . . . . 21
       
                          
                  |
89 | 88 | imp 436 |
. . . . . . . . . . . . . . . . . . . 20
                                                     |
90 | 89 | an32s 821 |
. . . . . . . . . . . . . . . . . . 19
         
    
                                      |
91 | | rmoim 3227 |
. . . . . . . . . . . . . . . . . . 19
 
                
                 |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         
    
                     
                 |
93 | 92 | expimpd 614 |
. . . . . . . . . . . . . . . . 17
        
                           

 
              |
94 | 93 | exlimdv 1787 |
. . . . . . . . . . . . . . . 16
        
                            
 
                |
95 | 66, 94 | syl5 32 |
. . . . . . . . . . . . . . 15
        
            
                 |
96 | 95 | impr 631 |
. . . . . . . . . . . . . 14
                       
               |
97 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
   |
98 | | nfmpt1 4485 |
. . . . . . . . . . . . . . . . 17
    
             |
99 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
   |
100 | 97, 98, 99 | nfbr 4440 |
. . . . . . . . . . . . . . . 16
                   |
101 | | nfv 1769 |
. . . . . . . . . . . . . . . 16
  
               |
102 | | breq1 4398 |
. . . . . . . . . . . . . . . . 17
                                       |
103 | | df-br 4396 |
. . . . . . . . . . . . . . . . . 18
    
            
  
  
              |
104 | | df-mpt 4456 |
. . . . . . . . . . . . . . . . . . 19
                  

                |
105 | 104 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . 18
      
                   
                 |
106 | | opabid 4708 |
. . . . . . . . . . . . . . . . . 18
       

               
                |
107 | 103, 105,
106 | 3bitri 279 |
. . . . . . . . . . . . . . . . 17
    
            

                |
108 | 102, 107 | syl6bb 269 |
. . . . . . . . . . . . . . . 16
                   
                 |
109 | 100, 101,
108 | cbvmo 2355 |
. . . . . . . . . . . . . . 15
                       
              |
110 | | df-rmo 2764 |
. . . . . . . . . . . . . . 15
              
  
                |
111 | 109, 110 | bitr4i 260 |
. . . . . . . . . . . . . 14
                   
               |
112 | 96, 111 | sylibr 217 |
. . . . . . . . . . . . 13
                                           |
113 | 112 | alrimiv 1781 |
. . . . . . . . . . . 12
                         
   
               |
114 | | dff12 5791 |
. . . . . . . . . . . 12
   
                   
                      
                |
115 | 58, 113, 114 | sylanbrc 677 |
. . . . . . . . . . 11
                         
                  |
116 | | f1domg 7607 |
. . . . . . . . . . 11
    
                   |
117 | 2, 115, 116 | mpsyl 64 |
. . . . . . . . . 10
                         |
118 | 117 | ex 441 |
. . . . . . . . 9
         
    
          |
119 | | difeq1 3533 |
. . . . . . . . . . . . 13
    
              |
120 | 119 | eleq2d 2534 |
. . . . . . . . . . . 12
    
     
          |
121 | 120 | ralbidv 2829 |
. . . . . . . . . . 11
    
 
    
   
       |
122 | 121 | anbi1d 719 |
. . . . . . . . . 10
    
  
             

     
    |
123 | 122 | imbi1d 324 |
. . . . . . . . 9
    
               
          
     |
124 | 118, 123 | syl5ibcom 228 |
. . . . . . . 8
              

     
     |
125 | 124 | ex 441 |
. . . . . . 7
     
    
  
       
     |
126 | 125 | exlimdv 1787 |
. . . . . 6
              

     
      |
127 | 3, 126 | syl5bi 225 |
. . . . 5
         

     
      |
128 | 127 | impd 438 |
. . . 4
       
  
       
    |
129 | 128 | rexlimiv 2867 |
. . 3
       
  
       
   |
130 | 1, 129 | sylbi 200 |
. 2

  
       
   |
131 | 130 | 3impib 1229 |
1
  
      
   |