Step | Hyp | Ref
| Expression |
1 | | snex 4112 |
. . . . . 6
 
 |
2 | 1 | elcompl 3226 |
. . . . 5
   ∼
 SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c    SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c  |
3 | 1 | elimak 4260 |
. . . . . 6
    SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c  1 1c     SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c   |
4 | | elpw11c 4148 |
. . . . . . . . . 10
 1 1c        |
5 | 4 | anbi1i 676 |
. . . . . . . . 9
  1
1c     
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c   
     
   SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
6 | | 19.41v 1901 |
. . . . . . . . 9
         
   SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c   
     
   SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
7 | 5, 6 | bitr4i 243 |
. . . . . . . 8
  1
1c     
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    
     
   SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
8 | 7 | exbii 1582 |
. . . . . . 7
    1 1c      SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c               
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
9 | | df-rex 2621 |
. . . . . . 7
 
1
1c    
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c
  
1 1c      SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
10 | | excom 1741 |
. . . . . . 7
               SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c               
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
11 | 8, 9, 10 | 3bitr4i 268 |
. . . . . 6
 
1
1c    
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c
             
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
12 | | snex 4112 |
. . . . . . . . . 10
     |
13 | | opkeq1 4060 |
. . . . . . . . . . 11
                     |
14 | 13 | eleq1d 2419 |
. . . . . . . . . 10
           SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c
        
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    |
15 | 12, 14 | ceqsexv 2895 |
. . . . . . . . 9
         
   SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c          
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c   |
16 | | elin 3220 |
. . . . . . . . 9
          SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c
          SIk Sk      
    Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c   |
17 | | snex 4112 |
. . . . . . . . . . . 12
 
 |
18 | | vex 2863 |
. . . . . . . . . . . 12
 |
19 | 17, 18 | opksnelsik 4266 |
. . . . . . . . . . 11
          SIk Sk      Sk  |
20 | | vex 2863 |
. . . . . . . . . . . 12
 |
21 | 20, 18 | elssetk 4271 |
. . . . . . . . . . 11
      Sk   |
22 | 19, 21 | bitri 240 |
. . . . . . . . . 10
          SIk Sk   |
23 | | opkex 4114 |
. . . . . . . . . . . . 13
        
 |
24 | 23 | elimak 4260 |
. . . . . . . . . . . 12
           Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  1 1 1 1c       
   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c   |
25 | | df-rex 2621 |
. . . . . . . . . . . 12
 
1 1 1
1c           
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c
  
1 1 1 1c            
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
26 | | elpw131c 4150 |
. . . . . . . . . . . . . . . 16
 1 1 1 1c            |
27 | 26 | anbi1i 676 |
. . . . . . . . . . . . . . 15
  1 1 1
1c            
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c   
                   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
28 | | 19.41v 1901 |
. . . . . . . . . . . . . . 15
                       
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c   
                   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
29 | 27, 28 | bitr4i 243 |
. . . . . . . . . . . . . 14
  1 1 1
1c            
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    
                   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
30 | 29 | exbii 1582 |
. . . . . . . . . . . . 13
    1 1 1 1c            
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c                
         
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
31 | | excom 1741 |
. . . . . . . . . . . . 13
                         
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c                
         
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
32 | 30, 31 | bitr4i 243 |
. . . . . . . . . . . 12
    1 1 1 1c            
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c                
         
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
33 | 24, 25, 32 | 3bitri 262 |
. . . . . . . . . . 11
           Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c     
                   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
34 | | snex 4112 |
. . . . . . . . . . . . . . 15
         |
35 | | opkeq1 4060 |
. . . . . . . . . . . . . . . 16
                              
            |
36 | 35 | eleq1d 2419 |
. . . . . . . . . . . . . . 15
                 
   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c
                   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    |
37 | 34, 36 | ceqsexv 2895 |
. . . . . . . . . . . . . 14
                       
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c                     
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c   |
38 | | eldif 3222 |
. . . . . . . . . . . . . 14
                
   
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c
                
   
Ins2k SIk Sk          
         
Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c   |
39 | | snex 4112 |
. . . . . . . . . . . . . . . . 17
     |
40 | 39, 12, 1 | otkelins2k 4256 |
. . . . . . . . . . . . . . . 16
                
   
Ins2k SIk Sk          SIk Sk  |
41 | | snex 4112 |
. . . . . . . . . . . . . . . . 17
 
 |
42 | 41, 18 | opksnelsik 4266 |
. . . . . . . . . . . . . . . 16
          SIk Sk      Sk  |
43 | | vex 2863 |
. . . . . . . . . . . . . . . . 17
 |
44 | 43, 18 | elssetk 4271 |
. . . . . . . . . . . . . . . 16
      Sk   |
45 | 40, 42, 44 | 3bitri 262 |
. . . . . . . . . . . . . . 15
                
   
Ins2k SIk Sk   |
46 | 39, 12, 1 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . 17
                
   
Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c      
    
   1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  |
47 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . 19
 
1
1c             
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    
1 1c                 1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
48 | | elpw11c 4148 |
. . . . . . . . . . . . . . . . . . . . . 22
 1 1c        |
49 | 48 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . 21
  1
1c              
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    
     
              1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
50 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . 21
         
              1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    
     
              1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
51 | 49, 50 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . 20
  1
1c              
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     
     
              1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
52 | 51 | exbii 1582 |
. . . . . . . . . . . . . . . . . . 19
    1 1c                 1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                         
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
53 | 47, 52 | bitri 240 |
. . . . . . . . . . . . . . . . . 18
 
1
1c             
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                        
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
54 | | opkex 4114 |
. . . . . . . . . . . . . . . . . . 19
            |
55 | 54 | elimak 4260 |
. . . . . . . . . . . . . . . . . 18
               1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  1 1c       
     
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    |
56 | | excom 1741 |
. . . . . . . . . . . . . . . . . 18
                 
     
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                         
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
57 | 53, 55, 56 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . 17
               1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c     
     
              1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
58 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . 21
     |
59 | | opkeq1 4060 |
. . . . . . . . . . . . . . . . . . . . . 22
            
     
                    |
60 | 59 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . 21
                      1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                   
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     |
61 | 58, 60 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . 20
         
              1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                    
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    |
62 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . 20
                     1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                      1 1 Nn k                   
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    |
63 | 58, 54 | opkelxpk 4249 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    1 1 Nn k       1 1 Nn               |
64 | 54, 63 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . . . 22
                    1 1 Nn k     
1 1 Nn  |
65 | | snelpw1 4147 |
. . . . . . . . . . . . . . . . . . . . . 22
     1 1 Nn  
1 Nn  |
66 | | snelpw1 4147 |
. . . . . . . . . . . . . . . . . . . . . 22
   1 Nn Nn  |
67 | 64, 65, 66 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . 21
                    1 1 Nn k  Nn  |
68 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . 22
                   Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c
                   Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                   Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   |
69 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
70 | 69, 39, 12 | otkelins2k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c         Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c  |
71 | | opkex 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        |
72 | 71 | elimak 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c  1 1 1c          Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk   |
73 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
1 1
1c         
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    1 1 1c           Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
74 | | elpw121c 4149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 1 1 1c          |
75 | 74 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  1 1
1c          
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
 
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
76 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
 
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
77 | 75, 76 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  1 1
1c          
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
  
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
78 | 77 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    1 1 1c          
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
                     Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
79 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
        Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
                     Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
80 | 78, 79 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    1 1 1c          
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
                     Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
81 | 72, 73, 80 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
82 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
83 | | opkeq1 4060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        
                          |
84 | 83 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk                
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
85 | 82, 84 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk   |
86 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk                  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
                Ins3k
Sk   |
87 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
 |
88 | 87, 69, 12 | otkelins2k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
   
    
SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c   |
89 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
90 | 89, 17 | opksnelsik 4266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
       1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c   |
91 | 89, 20 | eqpw1relk 4480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        1c k   Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
1   |
92 | 88, 90, 91 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
1   |
93 | 87, 69, 12 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 Ins3k Sk      Sk  |
94 | 89, 69 | elssetk 4271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      Sk   |
95 | 93, 94 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 Ins3k Sk   |
96 | 92, 95 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
                Ins3k
Sk  1
   |
97 | 85, 86, 96 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
 1
   |
98 | 97 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
        Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
  
1
   |
99 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 1
  
1
   |
100 | 98, 99 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
        Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
1   |
101 | 70, 81, 100 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c 1
  |
102 | | opkex 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        |
103 | 102 | elimak 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c  1 1 1c          Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk   |
104 | 74 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  1 1
1c          
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
 
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
105 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
 
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
106 | 104, 105 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  1 1
1c          
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
  
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
107 | 106 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    1 1 1c          
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
                     Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
108 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
1 1
1c         
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    1 1 1c           Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
109 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             
        Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
                     Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
110 | 107, 108,
109 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
1 1
1c         
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk     
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
111 | | opkeq1 4060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        
                          |
112 | 111 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk                
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk    |
113 | 82, 112 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
               
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk   |
114 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk                  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
                Ins3k
Sk   |
115 | 87, 69, 39 | otkelins2k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
   
    
SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c   |
116 | 89, 41 | opksnelsik 4266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
       1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c   |
117 | 89, 43 | eqpw1relk 4480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        1c k   Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
1   |
118 | 115, 116,
117 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
1   |
119 | 87, 69, 39 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 Ins3k Sk      Sk  |
120 | 119, 94 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 Ins3k Sk   |
121 | 118, 120 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
                Ins3k
Sk  1
   |
122 | 113, 114,
121 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
 1
   |
123 | 122 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
        Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk 
  
1
   |
124 | 103, 110,
123 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    1
   |
125 | 69, 39, 12 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c         Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c  |
126 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 1
  
1
   |
127 | 124, 125,
126 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c 1
  |
128 | 101, 127 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . 22
       
            Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c                   Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c
 1 1    |
129 | 68, 128 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
                   Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c
 1 1    |
130 | 67, 129 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . 20
       
             1 1 Nn k                   
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   Nn  1
1
    |
131 | 61, 62, 130 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
         
              1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    Nn  1
1
    |
132 | 131 | exbii 1582 |
. . . . . . . . . . . . . . . . . 18
                 
     
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c     
Nn  1 1     |
133 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . 18
 
Nn  1
1
    Nn  1
1
    |
134 | 132, 133 | bitr4i 243 |
. . . . . . . . . . . . . . . . 17
                 
     
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c    Nn  1
1
   |
135 | 46, 57, 134 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
                
   
Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  Nn  1
1
   |
136 | 135 | notbii 287 |
. . . . . . . . . . . . . . 15
                    
Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  Nn  1
1    |
137 | 45, 136 | anbi12i 678 |
. . . . . . . . . . . . . 14
                     
Ins2k SIk Sk          
         
Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c


Nn  1
1
    |
138 | 37, 38, 137 | 3bitri 262 |
. . . . . . . . . . . . 13
                       
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    Nn  1
1
    |
139 | 138 | exbii 1582 |
. . . . . . . . . . . 12
                         
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c    
 Nn  1
1     |
140 | | df-rex 2621 |
. . . . . . . . . . . 12
 
 Nn  1
1
     Nn  1
1
    |
141 | 139, 140 | bitr4i 243 |
. . . . . . . . . . 11
                         
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  
 Nn  1
1
   |
142 | | rexnal 2626 |
. . . . . . . . . . 11
 
 Nn  1
1
   Nn  1
1    |
143 | 33, 141, 142 | 3bitri 262 |
. . . . . . . . . 10
           Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c   Nn  1
1    |
144 | 22, 143 | anbi12i 678 |
. . . . . . . . 9
       
   SIk Sk      
    Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c



Nn  1
1
    |
145 | 15, 16, 144 | 3bitri 262 |
. . . . . . . 8
         
   SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    
Nn  1
1
    |
146 | 145 | exbii 1582 |
. . . . . . 7
               SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c    
  Nn  1
1     |
147 | | df-rex 2621 |
. . . . . . 7
 
 
Nn  1
1
     
Nn  1
1
    |
148 | 146, 147 | bitr4i 243 |
. . . . . 6
               SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  

 Nn  1
1
   |
149 | 3, 11, 148 | 3bitri 262 |
. . . . 5
    SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c   
Nn  1
1
   |
150 | 2, 149 | xchbinx 301 |
. . . 4
   ∼
 SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c  
 Nn  1
1
   |
151 | 18 | eluni1 4174 |
. . . 4
 ⋃1 ∼ 
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c   ∼  SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c  |
152 | | dfral2 2627 |
. . . 4
 


Nn  1
1
  
 Nn  1
1
   |
153 | 150, 151,
152 | 3bitr4i 268 |
. . 3
 ⋃1 ∼ 
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c 
 
Nn  1
1
   |
154 | 153 | eqabi 2465 |
. 2
⋃1 ∼  SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c
   
Nn  1
1
   |
155 | | ssetkex 4295 |
. . . . . . 7
Sk  |
156 | 155 | sikex 4298 |
. . . . . 6
SIk Sk  |
157 | 156 | ins2kex 4308 |
. . . . . . . 8
Ins2k SIk Sk  |
158 | | nncex 4397 |
. . . . . . . . . . . . . 14
Nn  |
159 | 158 | pw1ex 4304 |
. . . . . . . . . . . . 13
1 Nn  |
160 | 159 | pw1ex 4304 |
. . . . . . . . . . . 12
1 1 Nn  |
161 | | vvex 4110 |
. . . . . . . . . . . 12
 |
162 | 160, 161 | xpkex 4290 |
. . . . . . . . . . 11
 1 1 Nn
k
  |
163 | | 1cex 4143 |
. . . . . . . . . . . . . . . . . . . 20
1c
 |
164 | 163 | pwex 4330 |
. . . . . . . . . . . . . . . . . . 19
1c
 |
165 | 164, 161 | xpkex 4290 |
. . . . . . . . . . . . . . . . . 18
 1c k 
 |
166 | 155 | ins3kex 4309 |
. . . . . . . . . . . . . . . . . . . 20
Ins3k Sk  |
167 | 166, 157 | symdifex 4109 |
. . . . . . . . . . . . . . . . . . 19
Ins3k Sk Ins2k SIk Sk
 |
168 | 163 | pw1ex 4304 |
. . . . . . . . . . . . . . . . . . . . 21
1
1c
 |
169 | 168 | pw1ex 4304 |
. . . . . . . . . . . . . . . . . . . 20
1 1
1c
 |
170 | 169 | pw1ex 4304 |
. . . . . . . . . . . . . . . . . . 19
1 1 1
1c
 |
171 | 167, 170 | imakex 4301 |
. . . . . . . . . . . . . . . . . 18
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
172 | 165, 171 | difex 4108 |
. . . . . . . . . . . . . . . . 17
  1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
173 | 172 | sikex 4298 |
. . . . . . . . . . . . . . . 16
SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
174 | 173 | ins2kex 4308 |
. . . . . . . . . . . . . . 15
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
175 | 174, 166 | inex 4106 |
. . . . . . . . . . . . . 14
Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk
 |
176 | 175, 169 | imakex 4301 |
. . . . . . . . . . . . 13
 Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c
 |
177 | 176 | ins2kex 4308 |
. . . . . . . . . . . 12
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c
 |
178 | 176 | ins3kex 4309 |
. . . . . . . . . . . 12
Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c
 |
179 | 177, 178 | inex 4106 |
. . . . . . . . . . 11
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c
 |
180 | 162, 179 | inex 4106 |
. . . . . . . . . 10
  1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   |
181 | 180, 168 | imakex 4301 |
. . . . . . . . 9
   1 1 Nn k  Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c
 |
182 | 181 | ins3kex 4309 |
. . . . . . . 8
Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c
 |
183 | 157, 182 | difex 4108 |
. . . . . . 7
Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c
 |
184 | 183, 170 | imakex 4301 |
. . . . . 6
 Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c
 |
185 | 156, 184 | inex 4106 |
. . . . 5
SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c
 |
186 | 185, 168 | imakex 4301 |
. . . 4
 SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c
 |
187 | 186 | complex 4105 |
. . 3
∼  SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c
 |
188 | 187 | uni1ex 4294 |
. 2
⋃1 ∼  SIk Sk  Ins2k SIk Sk Ins3k    1 1 Nn k 
Ins2k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c Ins3k  Ins2k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins3k Sk  k 1 1 1c   k 1 1c  k 1 1 1 1c  k 1 1c
 |
189 | 154, 188 | eqeltrri 2424 |
1
   
Nn  1
1
   |