Step | Hyp | Ref
| Expression |
1 | | snex 4112 |
. . . . . . . . . 10
   |
2 | 1 | snid 3761 |
. . . . . . . . 9
       |
3 | | eqtfinrelk.2 |
. . . . . . . . . 10
 |
4 | 1, 3 | opkelxpk 4249 |
. . . . . . . . 9
           k      
         |
5 | 2, 4 | mpbiran 884 |
. . . . . . . 8
           k        |
6 | 3 | elsnc 3757 |
. . . . . . . 8
     |
7 | 5, 6 | bitri 240 |
. . . . . . 7
           k      |
8 | 7 | orbi1i 506 |
. . . . . 6
            k         ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k    
     ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      |
9 | | elun 3221 |
. . . . . 6
            k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k               k         ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      |
10 | 1, 3 | opkelxpk 4249 |
. . . . . . . . . . 11
           k 
  
       |
11 | 2, 3, 10 | mpbir2an 886 |
. . . . . . . . . 10
          k   |
12 | 11 | notnoti 115 |
. . . . . . . . 9
          k   |
13 | 12 | intnan 880 |
. . . . . . . 8
      ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c           k    |
14 | | eldif 3222 |
. . . . . . . 8
      ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k         ∼ 
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c           k     |
15 | 13, 14 | mtbir 290 |
. . . . . . 7
     ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k    |
16 | 15 | biorfi 396 |
. . . . . 6

      ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      |
17 | 8, 9, 16 | 3bitr4i 268 |
. . . . 5
            k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      |
18 | 17 | a1i 10 |
. . . 4

            k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
19 | | sneq 3745 |
. . . . . 6

 
    |
20 | 19 | opkeq1d 4066 |
. . . . 5

   
        |
21 | 20 | eleq1d 2419 |
. . . 4

            k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k               k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
22 | | iftrue 3669 |
. . . . 5

        Nn 
1      |
23 | 22 | eqeq2d 2364 |
. . . 4


 
      Nn 
1       |
24 | 18, 21, 23 | 3bitr4d 276 |
. . 3

            k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k            Nn 
1       |
25 | | iffalse 3670 |
. . . . 5
  
      Nn 
1        Nn 
1     |
26 | 25 | eqeq2d 2364 |
. . . 4
 
 
      Nn 
1        Nn 
1      |
27 | | opkex 4114 |
. . . . . . . . 9
   
  |
28 | 27 | elimak 4260 |
. . . . . . . 8
       Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c  1 1 1c       
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c   |
29 | | elpw121c 4149 |
. . . . . . . . . . . 12
 1 1 1c          |
30 | 29 | anbi1i 676 |
. . . . . . . . . . 11
  1 1
1c         Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c   
              Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
31 | | 19.41v 1901 |
. . . . . . . . . . 11
                  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c   
              Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
32 | 30, 31 | bitr4i 243 |
. . . . . . . . . 10
  1 1
1c         Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    
              Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
33 | 32 | exbii 1582 |
. . . . . . . . 9
    1 1 1c        
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c                    
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
34 | | df-rex 2621 |
. . . . . . . . 9
 
1 1
1c        Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c
  
1 1 1c        
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
35 | | excom 1741 |
. . . . . . . . 9
             
   
  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c                    
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
36 | 33, 34, 35 | 3bitr4i 268 |
. . . . . . . 8
 
1 1
1c        Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c
                  
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
37 | | snex 4112 |
. . . . . . . . . . 11
       |
38 | | opkeq1 4060 |
. . . . . . . . . . . 12
        
   
             
    |
39 | 38 | eleq1d 2419 |
. . . . . . . . . . 11
                Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c
             
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c    |
40 | 37, 39 | ceqsexv 2895 |
. . . . . . . . . 10
                  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c               
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c   |
41 | | elsymdif 3224 |
. . . . . . . . . . 11
            
  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c
               Ins2k Sk            
  Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c   |
42 | | snex 4112 |
. . . . . . . . . . . . . 14
 
 |
43 | | snex 4112 |
. . . . . . . . . . . . . 14
 
 |
44 | 42, 43, 3 | otkelins2k 4256 |
. . . . . . . . . . . . 13
            
  Ins2k Sk      Sk  |
45 | | vex 2863 |
. . . . . . . . . . . . . 14
 |
46 | 45, 3 | elssetk 4271 |
. . . . . . . . . . . . 13
      Sk   |
47 | 44, 46 | bitri 240 |
. . . . . . . . . . . 12
            
  Ins2k Sk   |
48 | | snex 4112 |
. . . . . . . . . . . . . . . 16
     |
49 | | opkeq1 4060 |
. . . . . . . . . . . . . . . . 17
                               |
50 | 49 | eleq1d 2419 |
. . . . . . . . . . . . . . . 16
               
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c          
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
51 | 48, 50 | ceqsexv 2895 |
. . . . . . . . . . . . . . 15
         
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c               
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c   |
52 | | eldif 3222 |
. . . . . . . . . . . . . . 15
              
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c               
Ins3k k Sk          
   
Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c   |
53 | | vex 2863 |
. . . . . . . . . . . . . . . . . 18
 |
54 | 53, 42, 43 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . 17
               Ins3k k
Sk  
   k
Sk  |
55 | 53, 42 | opkelcnvk 4251 |
. . . . . . . . . . . . . . . . 17
      k Sk
   
 Sk  |
56 | 45, 53 | elssetk 4271 |
. . . . . . . . . . . . . . . . 17
      Sk   |
57 | 54, 55, 56 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
               Ins3k k
Sk   |
58 | 53, 42, 43 | otkelins2k 4256 |
. . . . . . . . . . . . . . . . . 18
               Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c       Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  |
59 | | opkex 4114 |
. . . . . . . . . . . . . . . . . . . 20
      |
60 | 59 | elimak 4260 |
. . . . . . . . . . . . . . . . . . 19
       Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  1 1c       
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k   |
61 | | elpw11c 4148 |
. . . . . . . . . . . . . . . . . . . . . . 23
 1 1c        |
62 | 61 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . 22
  1
1c         Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k   
           
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
63 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . 22
         
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k   
           
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
64 | 62, 63 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . 21
  1
1c         Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k                
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
65 | 64 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . 20
    1 1c        
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k            
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
66 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . . 20
 
1
1c        Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    1 1c         Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
67 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . 20
                 
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k            
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
68 | 65, 66, 67 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . 19
 
1
1c        Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k     
     
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
69 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
70 | | opkeq1 4060 |
. . . . . . . . . . . . . . . . . . . . . . 23
            
              |
71 | 70 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . 22
             
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k      
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    |
72 | 69, 71 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . . 21
         
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k              Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k   |
73 | | elsymdif 3224 |
. . . . . . . . . . . . . . . . . . . . . 22
            
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k              Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
            Ins3k k
  |
74 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
75 | 74, 53, 43 | otkelins2k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
      Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c   |
76 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       Nn k 
 Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
      Nn k 
      Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c   |
77 | 74, 43 | opkelxpk 4249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      Nn k 
 Nn      |
78 | 43, 77 | mpbiran2 885 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      Nn k 
Nn  |
79 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
80 | | opkeq1 4060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                          
        |
81 | 80 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
                Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
82 | 79, 81 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                   
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c                  Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c   |
83 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
                
Ins2k SIk Sk                
Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c   |
84 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     |
85 | 84, 74, 43 | otkelins2k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                
Ins2k SIk Sk          SIk Sk  |
86 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
 |
87 | | eqtfinrelk.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
88 | 86, 87 | opksnelsik 4266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          SIk Sk      Sk  |
89 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
90 | 89, 87 | elssetk 4271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      Sk   |
91 | 85, 88, 90 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                
Ins2k SIk Sk   |
92 | | opkex 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
        |
93 | 92 | elimak 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
 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   |
94 | | elpw121c 4149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 1 1 1c          |
95 | 94 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  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    |
96 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                   
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    |
97 | 95, 96 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  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    |
98 | 97 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    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    |
99 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
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    |
100 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
             
        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    |
101 | 98, 99, 100 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
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    |
102 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
103 | | opkeq1 4060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
        
                     
    |
104 | 103 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 
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    |
105 | 102, 104 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                   
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   |
106 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 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   |
107 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
 |
108 | 107, 84, 74 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 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   |
109 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 |
110 | 109, 86 | opksnelsik 4266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
          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   |
111 | 109, 89 | eqpw1relk 4480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
        1c k   Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
1   |
112 | 108, 110,
111 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
1   |
113 | 107, 84, 74 | otkelins2k 4256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 Ins2k Sk      Sk  |
114 | 109, 74 | elssetk 4271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      Sk   |
115 | 113, 114 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 Ins2k Sk   |
116 | 112, 115 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
                Ins2k
Sk  1
   |
117 | 105, 106,
116 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                   
Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk 
 1
   |
118 | 117 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
        Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk 
  
1
   |
119 | 93, 101, 118 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       
 Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    1
   |
120 | 84, 74, 43 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                
Ins3k  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  |
121 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 1
  
1
   |
122 | 119, 120,
121 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                
Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c 1
  |
123 | 91, 122 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 
Ins2k SIk Sk                
Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
 1    |
124 | 82, 83, 123 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c   1    |
125 | 124 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                      Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    
1
   |
126 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
1 1 1
1c        Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
  
1 1 1 1c        
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
127 | | elpw131c 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 1 1 1 1c            |
128 | 127 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  1 1 1
1c         Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c   
               
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
129 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c   
               
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
130 | 128, 129 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  1 1 1
1c         Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    
               
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
131 | 130 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    1 1 1 1c        
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c                
      Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
132 | 126, 131 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
1 1 1
1c        Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c
              
      Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
133 | | opkex 4114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      |
134 | 133 | elimak 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c  1 1 1 1c       
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c   |
135 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                      Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c                
      Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
136 | 132, 134,
135 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c     
               
Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c    |
137 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
1   
1
   |
138 | 125, 136,
137 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c  1   |
139 | 78, 138 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       Nn k 
      Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
 Nn  1    |
140 | 75, 76, 139 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
            
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
 Nn  1    |
141 | 74, 53, 43 | otkelins3k 4257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
Ins3k k   
k  |
142 | | opkelidkg 4275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     k    |
143 | 74, 53, 142 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    k   |
144 | 141, 143 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
            
Ins3k k   |
145 | 140, 144 | bibi12i 306 |
. . . . . . . . . . . . . . . . . . . . . 22
       
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
            Ins3k k
  Nn  1
    |
146 | 73, 145 | xchbinx 301 |
. . . . . . . . . . . . . . . . . . . . 21
            
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k   Nn 
1     |
147 | 72, 146 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
         
      Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k    Nn  1
    |
148 | 147 | exbii 1582 |
. . . . . . . . . . . . . . . . . . 19
                 
Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k     Nn  1
    |
149 | 60, 68, 148 | 3bitri 262 |
. . . . . . . . . . . . . . . . . 18
       Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c   
Nn  1
    |
150 | | exnal 1574 |
. . . . . . . . . . . . . . . . . 18
    Nn 
1       Nn  1
    |
151 | 58, 149, 150 | 3bitrri 263 |
. . . . . . . . . . . . . . . . 17
     Nn 
1        
   
   
Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  |
152 | 151 | con1bii 321 |
. . . . . . . . . . . . . . . 16
      
   
   
Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c     Nn 
1     |
153 | 57, 152 | anbi12i 678 |
. . . . . . . . . . . . . . 15
       
   
   
Ins3k k Sk          
   
Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c      Nn  1
     |
154 | 51, 52, 153 | 3bitri 262 |
. . . . . . . . . . . . . 14
         
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c       Nn 
1      |
155 | 154 | exbii 1582 |
. . . . . . . . . . . . 13
                    Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    
    Nn  1
     |
156 | 42, 43, 3 | otkelins3k 4257 |
. . . . . . . . . . . . . 14
            
  Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c         Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  |
157 | | opkex 4114 |
. . . . . . . . . . . . . . 15
   
    |
158 | 157 | elimak 4260 |
. . . . . . . . . . . . . 14
       
 Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  1 1c          Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c   |
159 | | elpw11c 4148 |
. . . . . . . . . . . . . . . . . 18
 1 1c        |
160 | 159 | anbi1i 676 |
. . . . . . . . . . . . . . . . 17
  1
1c          
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c   
     
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
161 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . 17
         
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c   
     
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
162 | 160, 161 | bitr4i 243 |
. . . . . . . . . . . . . . . 16
  1
1c          
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    
     
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
163 | 162 | exbii 1582 |
. . . . . . . . . . . . . . 15
    1 1c          
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c                    
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
164 | | df-rex 2621 |
. . . . . . . . . . . . . . 15
 
1
1c         
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    1
1c          
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
165 | | excom 1741 |
. . . . . . . . . . . . . . 15
                    Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c                    
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
166 | 163, 164,
165 | 3bitr4i 268 |
. . . . . . . . . . . . . 14
 
1
1c         
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c           
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
167 | 156, 158,
166 | 3bitri 262 |
. . . . . . . . . . . . 13
            
  Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c     
     
   
   
Ins3k k Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c    |
168 | | dfiota2 4341 |
. . . . . . . . . . . . . . 15
    Nn 
1         Nn  1
    |
169 | 168 | eleq2i 2417 |
. . . . . . . . . . . . . 14
    
Nn  1
 
 
    Nn  1
     |
170 | | eluniab 3904 |
. . . . . . . . . . . . . 14
       Nn  1
          Nn 
1      |
171 | 169, 170 | bitri 240 |
. . . . . . . . . . . . 13
    
Nn  1
 
  
    Nn  1
     |
172 | 155, 167,
171 | 3bitr4i 268 |
. . . . . . . . . . . 12
            
  Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c     Nn 
1     |
173 | 47, 172 | bibi12i 306 |
. . . . . . . . . . 11
                Ins2k Sk            
  Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c
     Nn 
1      |
174 | 41, 173 | xchbinx 301 |
. . . . . . . . . 10
            
  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c

    Nn  1
     |
175 | 40, 174 | bitri 240 |
. . . . . . . . 9
                  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  
    Nn  1
     |
176 | 175 | exbii 1582 |
. . . . . . . 8
             
   
  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c   
    Nn  1
     |
177 | 28, 36, 176 | 3bitri 262 |
. . . . . . 7
       Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c  
    Nn  1
     |
178 | 177 | notbii 287 |
. . . . . 6
       Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c  
    Nn  1
     |
179 | 27 | elcompl 3226 |
. . . . . 6
      ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c     
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c  |
180 | | dfcleq 2347 |
. . . . . . 7
    
Nn  1
 
  
    Nn  1
     |
181 | | alex 1572 |
. . . . . . 7
   
    Nn  1
         Nn 
1      |
182 | 180, 181 | bitri 240 |
. . . . . 6
    
Nn  1
 
 
    Nn  1
     |
183 | 178, 179,
182 | 3bitr4i 268 |
. . . . 5
      ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c     Nn 
1     |
184 | 183 | a1i 10 |
. . . 4
       ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c     Nn 
1      |
185 | 43, 3 | opkelxpk 4249 |
. . . . . . . . . . 11
           k 
          |
186 | 3 | biantru 491 |
. . . . . . . . . . 11
         
       |
187 | 43 | elsnc 3757 |
. . . . . . . . . . . 12
             |
188 | 87 | sneqb 3877 |
. . . . . . . . . . . 12
       |
189 | 187, 188 | bitri 240 |
. . . . . . . . . . 11
         |
190 | 185, 186,
189 | 3bitr2i 264 |
. . . . . . . . . 10
           k 
  |
191 | 190 | biimpi 186 |
. . . . . . . . 9
           k 
  |
192 | 191 | con3i 127 |
. . . . . . . 8
           k    |
193 | 192 | biantrud 493 |
. . . . . . 7
       ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k      |
194 | | simpl 443 |
. . . . . . . . 9
     |
195 | 194 | con3i 127 |
. . . . . . . 8
 
   |
196 | | biorf 394 |
. . . . . . . 8
        
 ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k            ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k       |
197 | 195, 196 | syl 15 |
. . . . . . 7
       
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k            ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k       |
198 | 193, 197 | bitrd 244 |
. . . . . 6
       ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c         
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k       |
199 | 43, 3 | opkelxpk 4249 |
. . . . . . . 8
           k                |
200 | 189, 6 | anbi12i 678 |
. . . . . . . 8
       
   
   |
201 | 199, 200 | bitri 240 |
. . . . . . 7
           k    
   |
202 | | eldif 3222 |
. . . . . . 7
      ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k         ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k     |
203 | 201, 202 | orbi12i 507 |
. . . . . 6
            k   
   
 ∼ 
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k             ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c    
      k      |
204 | 198, 203 | syl6bbr 254 |
. . . . 5
       ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      
     k   
   
 ∼ 
Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
205 | | elun 3221 |
. . . . 5
            k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k               k         ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k      |
206 | 204, 205 | syl6bbr 254 |
. . . 4
       ∼
 Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c            k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k       |
207 | 26, 184, 206 | 3bitr2rd 273 |
. . 3
             k    ∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k            Nn 
1       |
208 | 24, 207 | pm2.61i 156 |
. 2
            k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k            Nn 
1      |
209 | | df-tfin 4444 |
. . 3
Tfin
 
      Nn 
1     |
210 | 209 | eqeq2i 2363 |
. 2
 Tfin
 
      Nn 
1      |
211 | 208, 210 | bitr4i 243 |
1
            k   
∼  Ins2k Sk Ins3k  Ins3k k
Sk Ins2k  Ins2k  Nn k   Ins2k SIk Sk Ins3k  Ins3k SIk   1c k 
 Ins3k Sk Ins2k SIk Sk  k 1 1 1 1c
Ins2k Sk  k 1 1 1c  k 1 1 1 1c
Ins3k k  k 1 1c  k 1 1c  k 1 1 1c      k    Tfin   |