Proof of Theorem proj1exg
Step | Hyp | Ref
| Expression |
1 | | dfproj12 4576 |
. 2
Proj1 kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k |
2 | | addcexlem 4382 |
. . . . . . . . 9
Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c
|
3 | | 1cex 4142 |
. . . . . . . . . . 11
1c
|
4 | 3 | pw1ex 4303 |
. . . . . . . . . 10
1
1c
|
5 | 4 | pw1ex 4303 |
. . . . . . . . 9
1 1
1c
|
6 | 2, 5 | imakex 4300 |
. . . . . . . 8
Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
|
7 | 6 | imagekex 4312 |
. . . . . . 7
Imagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c
|
8 | | nncex 4396 |
. . . . . . . 8
Nn |
9 | | vvex 4109 |
. . . . . . . 8
|
10 | 8, 9 | xpkex 4289 |
. . . . . . 7
Nn k
|
11 | 7, 10 | inex 4105 |
. . . . . 6
Imagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k |
12 | | idkex 4314 |
. . . . . . 7
k
|
13 | 8 | complex 4104 |
. . . . . . . 8
∼ Nn |
14 | 13, 9 | xpkex 4289 |
. . . . . . 7
∼ Nn k
|
15 | 12, 14 | inex 4105 |
. . . . . 6
k ∼ Nn k
|
16 | 11, 15 | unex 4106 |
. . . . 5
Imagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
17 | 16 | imagekex 4312 |
. . . 4
ImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
18 | 17 | cnvkex 4287 |
. . 3
kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k |
19 | | imakexg 4299 |
. . 3
kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k
|
20 | 18, 19 | mpan 651 |
. 2
kImagekImagek Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k ∼ Nn k k
|
21 | 1, 20 | syl5eqel 2437 |
1
Proj1 |