Step | Hyp | Ref
| Expression |
1 | | snidb 3987 |
. . . . 5

    |
2 | | fvres 5893 |
. . . . 5
                 |
3 | 1, 2 | sylbi 200 |
. . . 4
               |
4 | | fvprc 5873 |
. . . . 5
           |
5 | | fvprc 5873 |
. . . . 5
       |
6 | 4, 5 | eqtr4d 2508 |
. . . 4
               |
7 | 3, 6 | pm2.61i 169 |
. . 3
 
           |
8 | | funfv 5947 |
. . . 4
                          |
9 | | df-fun 5591 |
. . . . . . . . . . . . 13
    
 
         
      |
10 | 9 | simprbi 471 |
. . . . . . . . . . . 12
           
     |
11 | | ssdif0 3741 |
. . . . . . . . . . . 12
       
                  |
12 | 10, 11 | sylib 201 |
. . . . . . . . . . 11
                   |
13 | 12 | unieqd 4200 |
. . . . . . . . . 10
                     |
14 | | uni0 4217 |
. . . . . . . . . 10
  |
15 | 13, 14 | syl6eq 2521 |
. . . . . . . . 9
                    |
16 | 15 | unieqd 4200 |
. . . . . . . 8
                      |
17 | 16, 14 | syl6eq 2521 |
. . . . . . 7
                     |
18 | 17 | difeq2d 3540 |
. . . . . 6
                                     |
19 | | resima 5143 |
. . . . . . 7
 
               |
20 | | dif0 3749 |
. . . . . . 7
               |
21 | 19, 20 | eqtr4i 2496 |
. . . . . 6
 
                 |
22 | 18, 21 | syl6reqr 2524 |
. . . . 5
                                       |
23 | 22 | unieqd 4200 |
. . . 4
                            
    
       |
24 | 8, 23 | eqtrd 2505 |
. . 3
                                      |
25 | 7, 24 | syl5eqr 2519 |
. 2
                
                 |
26 | | nfunsn 5910 |
. . 3
           |
27 | | relres 5138 |
. . . . . . . . . . . . . . 15
     |
28 | | dffun3 5600 |
. . . . . . . . . . . . . . 15
    
 
               
    |
29 | 27, 28 | mpbiran 932 |
. . . . . . . . . . . . . 14
    
                |
30 | | iman 431 |
. . . . . . . . . . . . . . . . . . 19
        
      
   |
31 | 30 | albii 1699 |
. . . . . . . . . . . . . . . . . 18
     
     
          |
32 | | alnex 1673 |
. . . . . . . . . . . . . . . . . 18
    
   

            |
33 | 31, 32 | bitri 257 |
. . . . . . . . . . . . . . . . 17
     
             
   |
34 | 33 | exbii 1726 |
. . . . . . . . . . . . . . . 16
                  
   
   |
35 | | exnal 1707 |
. . . . . . . . . . . . . . . 16
           
      
   
   |
36 | 34, 35 | bitri 257 |
. . . . . . . . . . . . . . 15
            
      
   
   |
37 | 36 | albii 1699 |
. . . . . . . . . . . . . 14
             

               |
38 | | alnex 1673 |
. . . . . . . . . . . . . 14
        
   

                |
39 | 29, 37, 38 | 3bitrri 280 |
. . . . . . . . . . . . 13
         
   
       |
40 | 39 | con1bii 338 |
. . . . . . . . . . . 12
    
                |
41 | | sp 1957 |
. . . . . . . . . . . . 13
           

            |
42 | 41 | eximi 1715 |
. . . . . . . . . . . 12
         
   

      
   
   |
43 | 40, 42 | sylbi 200 |
. . . . . . . . . . 11
                   |
44 | | snssi 4107 |
. . . . . . . . . . . . . . . . . . . 20
             |
45 | | residm 5142 |
. . . . . . . . . . . . . . . . . . . . . 22
 
      
    |
46 | 45 | dmeqi 5041 |
. . . . . . . . . . . . . . . . . . . . 21
        
    |
47 | | ssdmres 5132 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  
 
          |
48 | 47 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . 21
   
               |
49 | 46, 48 | syl5eqr 2519 |
. . . . . . . . . . . . . . . . . . . 20
   
   
       |
50 | 44, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    
        |
51 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . 20
 |
52 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . 20
 |
53 | 51, 52 | breldm 5045 |
. . . . . . . . . . . . . . . . . . 19
      
      |
54 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . 21
      
          |
55 | | elsn 3973 |
. . . . . . . . . . . . . . . . . . . . 21
     |
56 | 54, 55 | syl6bb 269 |
. . . . . . . . . . . . . . . . . . . 20
      
        |
57 | 56 | biimpa 492 |
. . . . . . . . . . . . . . . . . . 19
       
    
  |
58 | 50, 53, 57 | syl2an 485 |
. . . . . . . . . . . . . . . . . 18
     
      
  |
59 | 58 | breq1d 4405 |
. . . . . . . . . . . . . . . . 17
     
                       |
60 | 59 | biimpd 212 |
. . . . . . . . . . . . . . . 16
     
             
         |
61 | 60 | ex 441 |
. . . . . . . . . . . . . . 15
       
          
          |
62 | 61 | pm2.43d 49 |
. . . . . . . . . . . . . 14
       
             |
63 | 62 | anim1d 574 |
. . . . . . . . . . . . 13
            

      
    |
64 | 63 | eximdv 1772 |
. . . . . . . . . . . 12
                    
   
    |
65 | 64 | exlimdv 1787 |
. . . . . . . . . . 11
            
   

             |
66 | 43, 65 | mpan9 477 |
. . . . . . . . . 10
      
        
   
   |
67 | 19 | eleq2i 2541 |
. . . . . . . . . . . . 13
                   |
68 | | elimasni 5201 |
. . . . . . . . . . . . 13
          
        |
69 | 67, 68 | sylbir 218 |
. . . . . . . . . . . 12
               |
70 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
71 | 70, 52 | uniop 4704 |
. . . . . . . . . . . . . . . 16
        |
72 | | opex 4664 |
. . . . . . . . . . . . . . . . . . 19
    |
73 | 72 | unisn 4205 |
. . . . . . . . . . . . . . . . . 18
     
    |
74 | 27 | brrelexi 4880 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  |
75 | | brcnvg 5020 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
    
   
         |
76 | 70, 74, 75 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
   
         |
77 | 76 | biimpar 493 |
. . . . . . . . . . . . . . . . . . . . . . 23
                        |
78 | 74 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
          
       |
79 | | breq2 4399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
       |
80 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
81 | 79, 80 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                             |
82 | 81 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                              |
83 | 78, 82 | mpancom 682 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
         
             |
84 | 83 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
         
             |
85 | 77, 84 | syldan 478 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 |
86 | 85 | anim1i 578 |
. . . . . . . . . . . . . . . . . . . . 21
          
       
   
              |
87 | 86 | an32s 821 |
. . . . . . . . . . . . . . . . . . . 20
                
 
         
        |
88 | | eldif 3400 |
. . . . . . . . . . . . . . . . . . . . 21
                                    |
89 | | rexv 3048 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
                        |
90 | 70, 52 | brco 5010 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 |
91 | | df-br 4396 |
. . . . . . . . . . . . . . . . . . . . . . 23
                              |
92 | 89, 90, 91 | 3bitr2ri 282 |
. . . . . . . . . . . . . . . . . . . . . 22
               
   
             |
93 | 52 | ideq 4992 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
94 | | df-br 4396 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  
 |
95 | | equcom 1870 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
96 | 93, 94, 95 | 3bitr3i 283 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
97 | 96 | notbii 303 |
. . . . . . . . . . . . . . . . . . . . . 22
   
  |
98 | 92, 97 | anbi12i 711 |
. . . . . . . . . . . . . . . . . . . . 21
                                       |
99 | 88, 98 | bitr2i 258 |
. . . . . . . . . . . . . . . . . . . 20
      
           
  
              |
100 | 87, 99 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
                
  
              |
101 | | snssi 4107 |
. . . . . . . . . . . . . . . . . . 19
                    
       
      |
102 | | uniss 4211 |
. . . . . . . . . . . . . . . . . . 19
        
    
   
              
      |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
                
                     |
104 | 73, 103 | syl5eqssr 3463 |
. . . . . . . . . . . . . . . . 17
                
  
               |
105 | 104 | unissd 4214 |
. . . . . . . . . . . . . . . 16
                
                    |
106 | 71, 105 | syl5eqssr 3463 |
. . . . . . . . . . . . . . 15
                
       
    
      |
107 | 70, 52 | prss 4117 |
. . . . . . . . . . . . . . 15
               
                 
                |
108 | 106, 107 | sylibr 217 |
. . . . . . . . . . . . . 14
                
          
   
         
       |
109 | 108 | simpld 466 |
. . . . . . . . . . . . 13
                
    
    
      |
110 | 109 | ex 441 |
. . . . . . . . . . . 12
                                 |
111 | 69, 110 | syl5 32 |
. . . . . . . . . . 11
               
    
    
       |
112 | 111 | exlimiv 1784 |
. . . . . . . . . 10
     
   

                
       |
113 | 66, 112 | syl 17 |
. . . . . . . . 9
      
                    
       |
114 | 113 | ssrdv 3424 |
. . . . . . . 8
      
                          |
115 | | ssdif0 3741 |
. . . . . . . 8
                                             |
116 | 114, 115 | sylib 201 |
. . . . . . 7
      
               
    
       |
117 | 116 | ex 441 |
. . . . . 6
      
                            |
118 | | ndmima 5211 |
. . . . . . . . 9
    
            |
119 | 19, 118 | syl5eqr 2519 |
. . . . . . . 8
    
        |
120 | 119 | difeq1d 3539 |
. . . . . . 7
    
      
                                 |
121 | | 0dif 3771 |
. . . . . . 7
     
    
      |
122 | 120, 121 | syl6eq 2521 |
. . . . . 6
    
      
                 |
123 | 117, 122 | pm2.61d1 164 |
. . . . 5
                
    
       |
124 | 123 | unieqd 4200 |
. . . 4
                 
    
        |
125 | 124, 14 | syl6eq 2521 |
. . 3
                 
    
       |
126 | 26, 125 | eqtr4d 2508 |
. 2
                                  |
127 | 25, 126 | pm2.61i 169 |
1
           
                |