Step | Hyp | Ref
| Expression |
1 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . 19
 
   |
2 | 1 | biimpac 489 |
. . . . . . . . . . . . . . . . . 18
 
   |
3 | | rabid 2967 |
. . . . . . . . . . . . . . . . . . 19
  

   |
4 | 3 | simplbi2com 633 |
. . . . . . . . . . . . . . . . . 18
       |
5 | 2, 4 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
       |
6 | 5 | impancom 442 |
. . . . . . . . . . . . . . . 16
 
  
    |
7 | 6 | ancrd 557 |
. . . . . . . . . . . . . . 15
 
   
     |
8 | 7 | expimpd 608 |
. . . . . . . . . . . . . 14
  

 
     |
9 | 8 | reximdv2 2858 |
. . . . . . . . . . . . 13
  
       |
10 | 9 | ralimia 2779 |
. . . . . . . . . . . 12
 


 
 
  |
11 | 3 | simplbi 462 |
. . . . . . . . . . . . . . . 16
     |
12 | 6 | pm4.71rd 641 |
. . . . . . . . . . . . . . . . 17
 
   

    |
13 | | df-mpt 4463 |
. . . . . . . . . . . . . . . . . . 19
       
      |
14 | 13 | breqi 4408 |
. . . . . . . . . . . . . . . . . 18
   
  
      

     |
15 | | df-br 4403 |
. . . . . . . . . . . . . . . . . 18
       
   
  
           |
16 | | opabid 4708 |
. . . . . . . . . . . . . . . . . 18
         
  
 
    |
17 | 14, 15, 16 | 3bitri 275 |
. . . . . . . . . . . . . . . . 17
   
  
 
    |
18 | 12, 17 | syl6bbr 267 |
. . . . . . . . . . . . . . . 16
 
    
      |
19 | 11, 18 | sylan2 477 |
. . . . . . . . . . . . . . 15
 

     
      |
20 | 19 | rexbidva 2898 |
. . . . . . . . . . . . . 14
  
    
    
      |
21 | 20 | ralbiia 2818 |
. . . . . . . . . . . . 13
 


   
           |
22 | | breq2 4406 |
. . . . . . . . . . . . . . . 16
    
     
      |
23 | 22 | rexbidv 2901 |
. . . . . . . . . . . . . . 15
  
          
    
      |
24 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
  
  |
25 | | nfrab1 2971 |
. . . . . . . . . . . . . . . 16
  
  |
26 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
27 | | nfmpt1 4492 |
. . . . . . . . . . . . . . . . 17
   
   |
28 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
29 | 26, 27, 28 | nfbr 4447 |
. . . . . . . . . . . . . . . 16
   
    |
30 | | nfv 1761 |
. . . . . . . . . . . . . . . 16
   
    |
31 | | breq1 4405 |
. . . . . . . . . . . . . . . 16
    
     
      |
32 | 24, 25, 29, 30, 31 | cbvrexf 3014 |
. . . . . . . . . . . . . . 15
            
    
     |
33 | 23, 32 | syl6bb 265 |
. . . . . . . . . . . . . 14
  
          
    
      |
34 | 33 | cbvralv 3019 |
. . . . . . . . . . . . 13
 


         
           |
35 | 21, 34 | bitr4i 256 |
. . . . . . . . . . . 12
 


   
           |
36 | 10, 35 | sylib 200 |
. . . . . . . . . . 11
 


 
          |
37 | | nfv 1761 |
. . . . . . . . . . . . . 14
   

  |
38 | 25 | nfcri 2586 |
. . . . . . . . . . . . . . 15
    |
39 | | nfcsb1v 3379 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
40 | 39 | nfeq2 2607 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)  |
41 | 38, 40 | nfan 2011 |
. . . . . . . . . . . . . 14
   

  ![]_ ]_](_urbrack.gif)   |
42 | | eleq1 2517 |
. . . . . . . . . . . . . . 15
   

    |
43 | | csbeq1a 3372 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
44 | 43 | eqeq2d 2461 |
. . . . . . . . . . . . . . 15
 
  ![]_ ]_](_urbrack.gif)    |
45 | 42, 44 | anbi12d 717 |
. . . . . . . . . . . . . 14
   

  
   ![]_ ]_](_urbrack.gif)     |
46 | 37, 41, 45 | cbvopab1 4473 |
. . . . . . . . . . . . 13
              
   ![]_ ]_](_urbrack.gif)    |
47 | | df-mpt 4463 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)    |
48 | 46, 13, 47 | 3eqtr4i 2483 |
. . . . . . . . . . . 12
     
   ![]_ ]_](_urbrack.gif)   |
49 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
50 | 39 | nfel1 2606 |
. . . . . . . . . . . . . 14
    ![]_ ]_](_urbrack.gif)
 |
51 | 43 | eleq1d 2513 |
. . . . . . . . . . . . . 14
 
  ![]_ ]_](_urbrack.gif)    |
52 | 26, 49, 50, 51 | elrabf 3194 |
. . . . . . . . . . . . 13
  

  ![]_ ]_](_urbrack.gif)    |
53 | 52 | simprbi 466 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)   |
54 | 48, 53 | fmpti 6045 |
. . . . . . . . . . 11
           |
55 | 36, 54 | jctil 540 |
. . . . . . . . . 10
 

            

           |
56 | | dffo4 6038 |
. . . . . . . . . 10
          
            

           |
57 | 55, 56 | sylibr 216 |
. . . . . . . . 9
 

            |
58 | 57 | adantl 468 |
. . . . . . . 8
      
 
    
     |
59 | | relen 7574 |
. . . . . . . . . . . . 13
 |
60 | 59 | brrelex2i 4876 |
. . . . . . . . . . . 12
   |
61 | | ssrab2 3514 |
. . . . . . . . . . . 12
   |
62 | | ssdomg 7615 |
. . . . . . . . . . . 12
  
      |
63 | 60, 61, 62 | mpisyl 21 |
. . . . . . . . . . 11
     |
64 | | ensym 7618 |
. . . . . . . . . . 11
   |
65 | | domentr 7628 |
. . . . . . . . . . 11
  
      |
66 | 63, 64, 65 | syl2anc 667 |
. . . . . . . . . 10
     |
67 | 66 | ad2antlr 733 |
. . . . . . . . 9
      

   |
68 | | enfi 7788 |
. . . . . . . . . . . 12
 
   |
69 | 68 | biimpac 489 |
. . . . . . . . . . 11
  
  |
70 | | rabfi 7796 |
. . . . . . . . . . 11
     |
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
   

  |
72 | | fodomfi 7850 |
. . . . . . . . . 10
  

               |
73 | 71, 57, 72 | syl2an 480 |
. . . . . . . . 9
      
    |
74 | | sbth 7692 |
. . . . . . . . 9
  
 
      |
75 | 67, 73, 74 | syl2anc 667 |
. . . . . . . 8
      

   |
76 | | simpll 760 |
. . . . . . . 8
      
  |
77 | | fofinf1o 7852 |
. . . . . . . 8
   
    
    
  
    
     |
78 | 58, 75, 76, 77 | syl3anc 1268 |
. . . . . . 7
      
 
    
     |
79 | | f1of1 5813 |
. . . . . . 7
          
 
    
     |
80 | 78, 79 | syl 17 |
. . . . . 6
      
 
    
     |
81 | | dff12 5778 |
. . . . . . . 8
          
                
      |
82 | 81 | simprbi 466 |
. . . . . . 7
                
     |
83 | 22 | mobidv 2320 |
. . . . . . . . 9
  
                |
84 | 29, 30, 31 | cbvmo 2335 |
. . . . . . . . 9
                 |
85 | 83, 84 | syl6bb 265 |
. . . . . . . 8
  
                |
86 | 85 | cbvalv 2116 |
. . . . . . 7
               
     |
87 | 82, 86 | sylib 200 |
. . . . . 6
                
     |
88 | | mormo 3007 |
. . . . . . 7
       

        |
89 | 88 | alimi 1684 |
. . . . . 6
         
  
  
     |
90 | | alral 2753 |
. . . . . 6
      
    
  
     |
91 | 80, 87, 89, 90 | 4syl 19 |
. . . . 5
      


        |
92 | 18 | rmobidva 2979 |
. . . . . 6
  

         |
93 | 92 | ralbiia 2818 |
. . . . 5
 

 
  
     |
94 | 91, 93 | sylibr 216 |
. . . 4
      


  |
95 | 94 | ex 436 |
. . 3
       
   |
96 | 95 | pm4.71d 640 |
. 2
               |
97 | | reu5 3008 |
. . . 4
 
 

   |
98 | 97 | ralbii 2819 |
. . 3
 

  

   |
99 | | r19.26 2917 |
. . 3
 
 

   
 
   |
100 | 98, 99 | bitri 253 |
. 2
 

 

     |
101 | 96, 100 | syl6bbr 267 |
1
      

   |