Step | Hyp | Ref
| Expression |
1 | | elex 2867 |
. 2
   |
2 | | elex 2867 |
. 2
   |
3 | | df-cok 4190 |
. . . . 5
 k   Ins2k Ins3k k  k  |
4 | 3 | eleq2i 2417 |
. . . 4
     k      Ins2k Ins3k
k  k   |
5 | | opkex 4113 |
. . . . 5
    |
6 | 5 | elimakv 4260 |
. . . 4
     Ins2k Ins3k k  k        
Ins2k Ins3k
k   |
7 | | vex 2862 |
. . . . . . . . . 10
 |
8 | | opkelins2kg 4251 |
. . . . . . . . . 10
   
         Ins2k                         |
9 | 7, 5, 8 | mp2an 653 |
. . . . . . . . 9
       Ins2k                        |
10 | | 3anass 938 |
. . . . . . . . . . . 12
                                   |
11 | 10 | 2exbii 1583 |
. . . . . . . . . . 11
               
        
                  |
12 | | 19.42vv 1907 |
. . . . . . . . . . 11
                     
                       |
13 | 11, 12 | bitri 240 |
. . . . . . . . . 10
               
                           |
14 | 13 | exbii 1582 |
. . . . . . . . 9
       
     
                         
       |
15 | 9, 14 | bitri 240 |
. . . . . . . 8
       Ins2k   
                      |
16 | 15 | anbi1i 676 |
. . . . . . 7
       
Ins2k       Ins3k k    
                     
   
Ins3k k   |
17 | | elin 3219 |
. . . . . . 7
       Ins2k Ins3k
k        Ins2k  
   
Ins3k k   |
18 | | 19.41v 1901 |
. . . . . . 7
                               Ins3k k    
                     
   
Ins3k k   |
19 | 16, 17, 18 | 3bitr4i 268 |
. . . . . 6
       Ins2k Ins3k
k                          
   
Ins3k k   |
20 | 19 | exbii 1582 |
. . . . 5
         Ins2k Ins3k
k                     
           Ins3k k   |
21 | | excom 1741 |
. . . . 5
                          
      Ins3k k                            
   
Ins3k k   |
22 | | anass 630 |
. . . . . . . 8
                        
   
Ins3k k                       
   
Ins3k k    |
23 | 22 | exbii 1582 |
. . . . . . 7
                               Ins3k k                              Ins3k k    |
24 | | snex 4111 |
. . . . . . . 8
     |
25 | | opkeq1 4059 |
. . . . . . . . . 10
                       |
26 | 25 | eleq1d 2419 |
. . . . . . . . 9
            Ins3k k           Ins3k k   |
27 | 26 | anbi2d 684 |
. . . . . . . 8
                            Ins3k k                           Ins3k k    |
28 | 24, 27 | ceqsexv 2894 |
. . . . . . 7
                         
   
Ins3k k                           
Ins3k k   |
29 | 23, 28 | bitri 240 |
. . . . . 6
                               Ins3k k            
             
Ins3k k   |
30 | 29 | exbii 1582 |
. . . . 5
                          
      Ins3k k                            
Ins3k k   |
31 | 20, 21, 30 | 3bitri 262 |
. . . 4
         Ins2k Ins3k
k                             Ins3k k   |
32 | 4, 6, 31 | 3bitri 262 |
. . 3
     k                              Ins3k k   |
33 | | ancom 437 |
. . . . 5
                           Ins3k k           
Ins3k k                   |
34 | | vex 2862 |
. . . . . . . 8
 |
35 | | otkelins3kg 4254 |
. . . . . . . 8
 
       
   
Ins3k k    k   |
36 | 34, 35 | mp3an1 1264 |
. . . . . . 7
 
           
Ins3k k    k   |
37 | | opkelcnvkg 4249 |
. . . . . . . . 9
 
     k       |
38 | 34, 37 | mpan 651 |
. . . . . . . 8
     k       |
39 | 38 | adantr 451 |
. . . . . . 7
 
     k       |
40 | 36, 39 | bitrd 244 |
. . . . . 6
 
           
Ins3k k       |
41 | | eqcom 2355 |
. . . . . . . . . 10
         
     |
42 | 41 | anbi1i 676 |
. . . . . . . . 9
                         |
43 | 42 | 2exbii 1583 |
. . . . . . . 8
                                 |
44 | | vex 2862 |
. . . . . . . . . . . . . 14
 |
45 | | vex 2862 |
. . . . . . . . . . . . . 14
 |
46 | | opkthg 4131 |
. . . . . . . . . . . . . 14
 
        
    |
47 | 44, 45, 46 | mp3an12 1267 |
. . . . . . . . . . . . 13
        
    |
48 | 47 | anbi1d 685 |
. . . . . . . . . . . 12
              
        |
49 | | anass 630 |
. . . . . . . . . . . 12
  
      
 
     |
50 | 48, 49 | syl6bb 252 |
. . . . . . . . . . 11
              
 
      |
51 | 50 | 2exbidv 1628 |
. . . . . . . . . 10
                               |
52 | 51 | adantl 452 |
. . . . . . . . 9
 
                               |
53 | | eeanv 1913 |
. . . . . . . . 9
      
 
    
          |
54 | 52, 53 | syl6bb 252 |
. . . . . . . 8
 
                  
           |
55 | 43, 54 | syl5bb 248 |
. . . . . . 7
 
                  
           |
56 | | elisset 2869 |
. . . . . . . . . 10
 
  |
57 | 56 | biantrurd 494 |
. . . . . . . . 9
                      |
58 | 57 | bicomd 192 |
. . . . . . . 8
      
               |
59 | | opkeq2 4060 |
. . . . . . . . . 10
         |
60 | 59 | eleq1d 2419 |
. . . . . . . . 9
           |
61 | 60 | ceqsexgv 2971 |
. . . . . . . 8
               |
62 | 58, 61 | sylan9bb 680 |
. . . . . . 7
 
   
              |
63 | 55, 62 | bitrd 244 |
. . . . . 6
 
                       |
64 | 40, 63 | anbi12d 691 |
. . . . 5
 
             Ins3k k                            |
65 | 33, 64 | syl5bb 248 |
. . . 4
 
             
             
Ins3k k      
     |
66 | 65 | exbidv 1626 |
. . 3
 
                              Ins3k k              |
67 | 32, 66 | syl5bb 248 |
. 2
 
      k               |
68 | 1, 2, 67 | syl2an 463 |
1
 
      k               |