Step | Hyp | Ref
| Expression |
1 | | imakeq2 4226 |
. 2
  k ∼  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
 k ∼  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   |
2 | | dfproj22 4578 |
. 2
Proj2  k ∼  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  |
3 | | dfproj22 4578 |
. 2
Proj2  k ∼  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  |
4 | 1, 2, 3 | 3eqtr4g 2410 |
1

Proj2
Proj2   |