Step | Hyp | Ref
| Expression |
1 | | opkex 4114 |
. . . . . 6
    |
2 | 1 | elimak 4260 |
. . . . 5
    ∼ 
Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c k 1 1c  1 1c      ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c  |
3 | | df-rex 2621 |
. . . . . 6
 
1
1c      ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c    1 1c      
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
4 | | elpw11c 4148 |
. . . . . . . . . 10
 1 1c        |
5 | 4 | anbi1i 676 |
. . . . . . . . 9
  1
1c       ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
 
     
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
6 | | 19.41v 1901 |
. . . . . . . . 9
         
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
 
     
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
7 | 5, 6 | bitr4i 243 |
. . . . . . . 8
  1
1c       ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
  
     
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
8 | 7 | exbii 1582 |
. . . . . . 7
    1 1c       ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
               ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
9 | | excom 1741 |
. . . . . . 7
                ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
               ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
10 | 8, 9 | bitr4i 243 |
. . . . . 6
    1 1c       ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
               ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
11 | 3, 10 | bitri 240 |
. . . . 5
 
1
1c      ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c     
     
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
12 | 2, 11 | bitri 240 |
. . . 4
    ∼ 
Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c k 1 1c     
     
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
13 | | snex 4112 |
. . . . . . 7
     |
14 | | opkeq1 4060 |
. . . . . . . 8
                       |
15 | 14 | eleq1d 2419 |
. . . . . . 7
            ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c      
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c   |
16 | 13, 15 | ceqsexv 2895 |
. . . . . 6
         
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
          ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c  |
17 | | vex 2863 |
. . . . . . 7
 |
18 | | vex 2863 |
. . . . . . 7
 |
19 | | vex 2863 |
. . . . . . 7
 |
20 | 17, 18, 19 | setconslem7 4738 |
. . . . . 6
           ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c      |
21 | 16, 20 | bitri 240 |
. . . . 5
         
   
∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c
     |
22 | 21 | exbii 1582 |
. . . 4
                ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c

     |
23 | 12, 22 | bitri 240 |
. . 3
    ∼ 
Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c k 1 1c       |
24 | 23 | opabbii 4627 |
. 2
  
    ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c k 1 1c   
 
     |
25 | | setconslem4 4735 |
. 2
⋃1⋃1    k 
k
 k ∼ 
Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins2k  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c  k ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c k 1 1c
       ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c k 1 1c  |
26 | | df-1st 4724 |
. 2
          |
27 | 24, 25, 26 | 3eqtr4ri 2384 |
1
⋃1⋃1    k 
k
 k ∼ 
Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins2k  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c  k ∼  Ins2k Ins3k Sk Ins2k Ins2k Sk k SIk kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k     Ins3k SIk SIk  Ins2k Sk Ins3k SIk ∼  Ins2k Sk Ins3k   kImagek Imagek Ins3k ∼  Ins3k Sk Ins2k Sk  k 1 1 1c  Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk   k 1 1 1 1 1c  k 1 1 1c Nn k   k ∼ Nn k    k Sk   0c k     k 1 1 1c  k 1 1 1c   k 1 1 1 1 1c k 1 1c  |