Proof of Theorem proj2exg
Step | Hyp | Ref
| Expression |
1 | | dfproj22 4577 |
. 2
Proj2 k ∼ Ins2k Sk Ins3k 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 Sk 0c k k1 1 1ck |
2 | | ssetkex 4294 |
. . . . . . . 8
Sk |
3 | 2 | ins2kex 4307 |
. . . . . . 7
Ins2k Sk |
4 | | addcexlem 4382 |
. . . . . . . . . . . . . . . 16
Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c
|
5 | | 1cex 4142 |
. . . . . . . . . . . . . . . . . 18
1c
|
6 | 5 | pw1ex 4303 |
. . . . . . . . . . . . . . . . 17
1
1c
|
7 | 6 | pw1ex 4303 |
. . . . . . . . . . . . . . . 16
1 1
1c
|
8 | 4, 7 | imakex 4300 |
. . . . . . . . . . . . . . 15
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
|
9 | 8 | imagekex 4312 |
. . . . . . . . . . . . . 14
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
|
10 | | nncex 4396 |
. . . . . . . . . . . . . . 15
Nn |
11 | | vvex 4109 |
. . . . . . . . . . . . . . 15
|
12 | 10, 11 | xpkex 4289 |
. . . . . . . . . . . . . 14
Nn k
|
13 | 9, 12 | inex 4105 |
. . . . . . . . . . . . 13
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 |
14 | | idkex 4314 |
. . . . . . . . . . . . . 14
k
|
15 | 10 | complex 4104 |
. . . . . . . . . . . . . . 15
∼ Nn |
16 | 15, 11 | xpkex 4289 |
. . . . . . . . . . . . . 14
∼ Nn k
|
17 | 14, 16 | inex 4105 |
. . . . . . . . . . . . 13
k ∼ Nn k
|
18 | 13, 17 | unex 4106 |
. . . . . . . . . . . 12
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 |
19 | 18 | imagekex 4312 |
. . . . . . . . . . 11
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 |
20 | 19 | cnvkex 4287 |
. . . . . . . . . 10
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 |
21 | 20, 2 | cokex 4310 |
. . . . . . . . 9
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 Sk
|
22 | | snex 4111 |
. . . . . . . . . 10
0c
|
23 | 22, 11 | xpkex 4289 |
. . . . . . . . 9
0c k
|
24 | 21, 23 | unex 4106 |
. . . . . . . 8
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 Sk 0c k |
25 | 24 | ins3kex 4308 |
. . . . . . 7
Ins3k 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 Sk 0c k |
26 | 3, 25 | symdifex 4108 |
. . . . . 6
Ins2k Sk Ins3k 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 Sk 0c k |
27 | 26, 7 | imakex 4300 |
. . . . 5
Ins2k Sk Ins3k 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 Sk 0c k k1 1 1c |
28 | 27 | complex 4104 |
. . . 4
∼ Ins2k Sk Ins3k 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 Sk 0c k k1 1 1c |
29 | 28 | cnvkex 4287 |
. . 3
k
∼ Ins2k Sk Ins3k 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 Sk 0c k k1 1 1c |
30 | | imakexg 4299 |
. . 3
k ∼
Ins2k Sk Ins3k 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 Sk 0c k k1 1 1c k
∼ Ins2k Sk Ins3k 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 Sk 0c k k1 1 1ck
|
31 | 29, 30 | mpan 651 |
. 2
k ∼ Ins2k Sk Ins3k 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 Sk 0c k k1 1 1ck
|
32 | 1, 31 | syl5eqel 2437 |
1
Proj2 |