Step | Hyp | Ref
| Expression |
1 | | df-proj2 4569 |
. 2
Proj2  Phi 0c   |
2 | | vex 2863 |
. . . . . . 7
 |
3 | | vex 2863 |
. . . . . . 7
 |
4 | 2, 3 | opkelcnvk 4251 |
. . . . . 6
    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    ∼
 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  |
5 | | dfop2lem1 4574 |
. . . . . 6
    ∼  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 Phi 0c   |
6 | 4, 5 | bitri 240 |
. . . . 5
    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 Phi 0c   |
7 | 6 | rexbii 2640 |
. . . 4
 
  
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  Phi 0c   |
8 | 3 | elimak 4260 |
. . . 4
  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  |
9 | | risset 2662 |
. . . 4
 Phi 0c  Phi 0c   |
10 | 7, 8, 9 | 3bitr4i 268 |
. . 3
  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 Phi 0c   |
11 | 10 | eqabi 2465 |
. 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
 Phi 0c   |
12 | 1, 11 | eqtr4i 2376 |
1
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  |