Step | Hyp | Ref
| Expression |
1 | | vex 2741 |
. . . . . . . . . 10
 |
2 | | eqeq1 2184 |
. . . . . . . . . . 11
 
   |
3 | 2 | rexbidv 2478 |
. . . . . . . . . 10
  

   |
4 | 1, 3 | elab 2882 |
. . . . . . . . 9
  
    |
5 | | r19.29 2614 |
. . . . . . . . . 10
         
   

       
     |
6 | | nfv 1528 |
. . . . . . . . . . . 12
  
   |
7 | | nfre1 2520 |
. . . . . . . . . . . . . 14
  
 |
8 | 7 | nfab 2324 |
. . . . . . . . . . . . 13
   
  |
9 | | nfv 1528 |
. . . . . . . . . . . . 13
  
  |
10 | 8, 9 | nfralxy 2515 |
. . . . . . . . . . . 12
  
   
  |
11 | 6, 10 | nfan 1565 |
. . . . . . . . . . 11
        
     |
12 | | f1eq1 5417 |
. . . . . . . . . . . . . . . 16
             |
13 | 12 | biimparc 299 |
. . . . . . . . . . . . . . 15
     

      |
14 | | df-f1 5222 |
. . . . . . . . . . . . . . . 16
    
         |
15 | | ffun 5369 |
. . . . . . . . . . . . . . . . 17
       |
16 | 15 | anim1i 340 |
. . . . . . . . . . . . . . . 16
             |
17 | 14, 16 | sylbi 121 |
. . . . . . . . . . . . . . 15
     
    |
18 | 13, 17 | syl 14 |
. . . . . . . . . . . . . 14
     

     |
19 | 18 | adantlr 477 |
. . . . . . . . . . . . 13
        
        |
20 | | vex 2741 |
. . . . . . . . . . . . . . . 16
 |
21 | | eqeq1 2184 |
. . . . . . . . . . . . . . . . 17
 
   |
22 | 21 | rexbidv 2478 |
. . . . . . . . . . . . . . . 16
  

   |
23 | 20, 22 | elab 2882 |
. . . . . . . . . . . . . . 15
  
    |
24 | | fun11iun.1 |
. . . . . . . . . . . . . . . . . 18
   |
25 | 24 | eqeq2d 2189 |
. . . . . . . . . . . . . . . . 17
 
   |
26 | 25 | cbvrexv 2705 |
. . . . . . . . . . . . . . . 16
 

  |
27 | | r19.29 2614 |
. . . . . . . . . . . . . . . . . . 19
   
   
 

   |
28 | | sseq12 3181 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     |
29 | 28 | ancoms 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
30 | | sseq12 3181 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
31 | 29, 30 | orbi12d 793 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  

     |
32 | 31 | biimprcd 160 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
    |
33 | 32 | expdimp 259 |
. . . . . . . . . . . . . . . . . . . . 21
  
 

     |
34 | 33 | rexlimivw 2590 |
. . . . . . . . . . . . . . . . . . . 20
   
 

     |
35 | 34 | imp 124 |
. . . . . . . . . . . . . . . . . . 19
    

  
   |
36 | 27, 35 | sylan 283 |
. . . . . . . . . . . . . . . . . 18
    


  
   |
37 | 36 | an32s 568 |
. . . . . . . . . . . . . . . . 17
    

 
 
   |
38 | 37 | adantlll 480 |
. . . . . . . . . . . . . . . 16
       

  
 
 
   |
39 | 26, 38 | sylan2b 287 |
. . . . . . . . . . . . . . 15
       

  
 
 
   |
40 | 23, 39 | sylan2b 287 |
. . . . . . . . . . . . . 14
       

  

    
   |
41 | 40 | ralrimiva 2550 |
. . . . . . . . . . . . 13
        
     
     |
42 | 19, 41 | jca 306 |
. . . . . . . . . . . 12
        
    
  
 
 
    |
43 | 42 | a1i 9 |
. . . . . . . . . . 11
       

  
       
       |
44 | 11, 43 | rexlimi 2587 |
. . . . . . . . . 10
         
    
  
 
 
    |
45 | 5, 44 | syl 14 |
. . . . . . . . 9
         
   
    
 
 
    |
46 | 4, 45 | sylan2b 287 |
. . . . . . . 8
         
   
   
  
 
 
    |
47 | 46 | ralrimiva 2550 |
. . . . . . 7
 
      
    

    
 
 
    |
48 | | fun11uni 5287 |
. . . . . . 7
 
 
       
    
       
    |
49 | 47, 48 | syl 14 |
. . . . . 6
 
      
     
    
    |
50 | 49 | simpld 112 |
. . . . 5
 
      
 
      |
51 | | fun11iun.2 |
. . . . . . 7
 |
52 | 51 | dfiun2 3921 |
. . . . . 6

  
  |
53 | 52 | funeqi 5238 |
. . . . 5
 
      |
54 | 50, 53 | sylibr 134 |
. . . 4
 
      
 
   |
55 | | nfra1 2508 |
. . . . . . 7
  
      
   |
56 | | rsp 2524 |
. . . . . . . . 9
 
      
  
    

      |
57 | 1 | eldm2 4826 |
. . . . . . . . . . 11

       |
58 | | f1dm 5427 |
. . . . . . . . . . . 12
       |
59 | 58 | eleq2d 2247 |
. . . . . . . . . . 11
         |
60 | 57, 59 | bitr3id 194 |
. . . . . . . . . 10
          
   |
61 | 60 | adantr 276 |
. . . . . . . . 9
       
       
   |
62 | 56, 61 | syl6 33 |
. . . . . . . 8
 
      
  
     
    |
63 | 62 | imp 124 |
. . . . . . 7
         
  
     
   |
64 | 55, 63 | rexbida 2472 |
. . . . . 6
 
      
   
    

   |
65 | | eliun 3891 |
. . . . . . . 8
           |
66 | 65 | exbii 1605 |
. . . . . . 7
      
  
     |
67 | 1 | eldm2 4826 |
. . . . . . 7
 
        |
68 | | rexcom4 2761 |
. . . . . . 7
      
  
     |
69 | 66, 67, 68 | 3bitr4i 212 |
. . . . . 6
 

       |
70 | | eliun 3891 |
. . . . . 6
 

  |
71 | 64, 69, 70 | 3bitr4g 223 |
. . . . 5
 
      
    
   |
72 | 71 | eqrdv 2175 |
. . . 4
 
      
 
 
  |
73 | | df-fn 5220 |
. . . 4
 
  

    |
74 | 54, 72, 73 | sylanbrc 417 |
. . 3
 
      
  
   |
75 | | rniun 5040 |
. . . 4

  |
76 | | f1rn 5423 |
. . . . . . 7
    
  |
77 | 76 | adantr 276 |
. . . . . 6
       
 
  |
78 | 77 | ralimi 2540 |
. . . . 5
 
      
  
  |
79 | | iunss 3928 |
. . . . 5
 

  |
80 | 78, 79 | sylibr 134 |
. . . 4
 
      
  
  |
81 | 75, 80 | eqsstrid 3202 |
. . 3
 
      
 
   |
82 | | df-f 5221 |
. . 3
 
      
     |
83 | 74, 81, 82 | sylanbrc 417 |
. 2
 
      
          |
84 | 49 | simprd 114 |
. . 3
 
      
 
   
   |
85 | 52 | cnveqi 4803 |
. . . 4
 
   
  |
86 | 85 | funeqi 5238 |
. . 3
      
   |
87 | 84, 86 | sylibr 134 |
. 2
 
      
 
 
  |
88 | | df-f1 5222 |
. 2
 
    
 
  
       |
89 | 83, 87, 88 | sylanbrc 417 |
1
 
      
          |