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

   |
123 | 122 | rexbii 2640 |
. . . . . . . . . . . . . . 15
 
Nn                 
Ins2k k Sk Ins3k k Sk 
 Nn 
   |
124 | 98, 106, 123 | 3bitri 262 |
. . . . . . . . . . . . . 14
       
 Ins2k k
Sk Ins3k k Sk  k 1 1 Nn 
Nn 
   |
125 | 95, 96, 124 | 3bitri 262 |
. . . . . . . . . . . . 13
                
  Ins3k
SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn 
Nn 
   |
126 | 125 | notbii 287 |
. . . . . . . . . . . 12
                   Ins3k
SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn  Nn 
   |
127 | 94, 126 | anbi12i 678 |
. . . . . . . . . . 11
                      k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
               
  Ins3k
SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn    1 1   Nn 
    |
128 | 28, 29, 127 | 3bitri 262 |
. . . . . . . . . 10
                         k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn  
  1 1   Nn      |
129 | 128 | exbii 1582 |
. . . . . . . . 9
                       
   k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn  
    1
1
  Nn 
    |
130 | 16, 24, 129 | 3bitri 262 |
. . . . . . . 8
       
    k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c     1
1
  Nn 
    |
131 | | exanali 1585 |
. . . . . . . 8
     1 1   Nn 
 
    1
1
  Nn      |
132 | 14, 130, 131 | 3bitri 262 |
. . . . . . 7
         
     k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c
    1
1
  Nn      |
133 | 132 | exbii 1582 |
. . . . . 6
            
    k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c
     1
1
  Nn      |
134 | 2, 10, 133 | 3bitri 262 |
. . . . 5
      k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c      1 1  
Nn 
    |
135 | 134 | notbii 287 |
. . . 4
      k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c      1
1   Nn 
    |
136 | 1 | elcompl 3226 |
. . . 4
 ∼      k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c      k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c  |
137 | | alex 1572 |
. . . 4
       1
1
  Nn         1
1
  Nn      |
138 | 135, 136,
137 | 3bitr4i 268 |
. . 3
 ∼      k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c       1
1
  Nn      |
139 | 138 | eqabi 2465 |
. 2
∼      k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c
       1
1
  Nn      |
140 | | vvex 4110 |
. . . . . . . 8
 |
141 | | 1cex 4143 |
. . . . . . . . . . . . . . 15
1c
 |
142 | 141 | pwex 4330 |
. . . . . . . . . . . . . 14
1c
 |
143 | 142, 140 | xpkex 4290 |
. . . . . . . . . . . . 13
 1c k 
 |
144 | | ssetkex 4295 |
. . . . . . . . . . . . . . . 16
Sk  |
145 | 144 | ins3kex 4309 |
. . . . . . . . . . . . . . 15
Ins3k Sk  |
146 | 144 | sikex 4298 |
. . . . . . . . . . . . . . . 16
SIk Sk  |
147 | 146 | ins2kex 4308 |
. . . . . . . . . . . . . . 15
Ins2k SIk Sk  |
148 | 145, 147 | symdifex 4109 |
. . . . . . . . . . . . . 14
Ins3k Sk Ins2k SIk Sk
 |
149 | 141 | pw1ex 4304 |
. . . . . . . . . . . . . . . 16
1
1c
 |
150 | 149 | pw1ex 4304 |
. . . . . . . . . . . . . . 15
1 1
1c
 |
151 | 150 | pw1ex 4304 |
. . . . . . . . . . . . . 14
1 1 1
1c
 |
152 | 148, 151 | imakex 4301 |
. . . . . . . . . . . . 13
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
153 | 143, 152 | difex 4108 |
. . . . . . . . . . . 12
  1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
154 | 153 | sikex 4298 |
. . . . . . . . . . 11
SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
155 | 154 | ins3kex 4309 |
. . . . . . . . . 10
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
 |
156 | 144 | ins2kex 4308 |
. . . . . . . . . 10
Ins2k Sk  |
157 | 155, 156 | inex 4106 |
. . . . . . . . 9
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk
 |
158 | 157, 150 | imakex 4301 |
. . . . . . . 8
 Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
 |
159 | 140, 158 | xpkex 4290 |
. . . . . . 7
 k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
 |
160 | 158 | ins2kex 4308 |
. . . . . . 7
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
 |
161 | 159, 160 | inex 4106 |
. . . . . 6
  k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
 |
162 | 144 | cnvkex 4288 |
. . . . . . . . . . 11
k
Sk  |
163 | 162 | ins2kex 4308 |
. . . . . . . . . 10
Ins2k k Sk  |
164 | 162 | ins3kex 4309 |
. . . . . . . . . 10
Ins3k k Sk  |
165 | 163, 164 | inex 4106 |
. . . . . . . . 9
Ins2k k Sk Ins3k k Sk
 |
166 | | nncex 4397 |
. . . . . . . . . . 11
Nn  |
167 | 166 | pw1ex 4304 |
. . . . . . . . . 10
1 Nn  |
168 | 167 | pw1ex 4304 |
. . . . . . . . 9
1 1 Nn  |
169 | 165, 168 | imakex 4301 |
. . . . . . . 8
 Ins2k k Sk Ins3k k Sk  k 1 1 Nn  |
170 | 169 | sikex 4298 |
. . . . . . 7
SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn  |
171 | 170 | ins3kex 4309 |
. . . . . 6
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn  |
172 | 161, 171 | difex 4108 |
. . . . 5
   k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn 
 |
173 | 172, 151 | imakex 4301 |
. . . 4
    k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c
 |
174 | 173, 149 | imakex 4301 |
. . 3
     k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c
 |
175 | 174 | complex 4105 |
. 2
∼      k 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins2k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
Ins3k SIk  Ins2k k
Sk Ins3k k Sk  k 1 1 Nn   k 1 1 1 1c k 1 1c
 |
176 | 139, 175 | eqeltrri 2424 |
1
       1
1
  Nn      |