Proof of Theorem setconslem5
Step | Hyp | Ref
| Expression |
1 | | ssetkex 4294 |
. . . . . . 7
Sk |
2 | 1 | sikex 4297 |
. . . . . 6
SIk Sk |
3 | 2 | sikex 4297 |
. . . . 5
SIk SIk Sk |
4 | 3 | ins3kex 4308 |
. . . 4
Ins3k SIk SIk Sk |
5 | | addcexlem 4382 |
. . . . . . . . . . . . . . 15
Ins3k ∼ Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1c
|
6 | | 1cex 4142 |
. . . . . . . . . . . . . . . . 17
1c
|
7 | 6 | pw1ex 4303 |
. . . . . . . . . . . . . . . 16
1
1c
|
8 | 7 | pw1ex 4303 |
. . . . . . . . . . . . . . 15
1 1
1c
|
9 | 5, 8 | imakex 4300 |
. . . . . . . . . . . . . 14
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 | 9 | imagekex 4312 |
. . . . . . . . . . . . 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
|
11 | | nncex 4396 |
. . . . . . . . . . . . . 14
Nn |
12 | | vvex 4109 |
. . . . . . . . . . . . . 14
|
13 | 11, 12 | xpkex 4289 |
. . . . . . . . . . . . 13
Nn k
|
14 | 10, 13 | inex 4105 |
. . . . . . . . . . . 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 |
15 | | idkex 4314 |
. . . . . . . . . . . . 13
k
|
16 | 11 | complex 4104 |
. . . . . . . . . . . . . 14
∼ Nn |
17 | 16, 12 | xpkex 4289 |
. . . . . . . . . . . . 13
∼ Nn k
|
18 | 15, 17 | inex 4105 |
. . . . . . . . . . . 12
k ∼ Nn k
|
19 | 14, 18 | unex 4106 |
. . . . . . . . . . 11
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 |
20 | 19 | imagekex 4312 |
. . . . . . . . . 10
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 |
21 | 20 | cnvkex 4287 |
. . . . . . . . 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 |
22 | 21 | sikex 4297 |
. . . . . . . 8
SIk 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 |
23 | 1, 22 | cokex 4310 |
. . . . . . 7
Sk k SIk 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 |
24 | 23 | ins3kex 4308 |
. . . . . 6
Ins3k Sk k SIk 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 |
25 | 1 | ins2kex 4307 |
. . . . . . . . 9
Ins2k Sk |
26 | 21, 1 | cokex 4310 |
. . . . . . . . . . . . . . . 16
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
|
27 | | snex 4111 |
. . . . . . . . . . . . . . . . 17
0c
|
28 | 27, 12 | xpkex 4289 |
. . . . . . . . . . . . . . . 16
0c k
|
29 | 26, 28 | unex 4106 |
. . . . . . . . . . . . . . 15
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 |
30 | 29 | ins3kex 4308 |
. . . . . . . . . . . . . 14
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 |
31 | 25, 30 | symdifex 4108 |
. . . . . . . . . . . . 13
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 |
32 | 31, 8 | imakex 4300 |
. . . . . . . . . . . 12
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 |
33 | 32 | complex 4104 |
. . . . . . . . . . 11
∼ 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 |
34 | 33 | sikex 4297 |
. . . . . . . . . 10
SIk ∼ 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 |
35 | 34 | ins3kex 4308 |
. . . . . . . . 9
Ins3k SIk ∼ 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 |
36 | 25, 35 | inex 4105 |
. . . . . . . 8
Ins2k Sk Ins3k SIk ∼ 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 |
37 | 36, 8 | imakex 4300 |
. . . . . . 7
Ins2k Sk Ins3k SIk ∼ 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 1ck1 1 1c |
38 | 37 | ins2kex 4307 |
. . . . . 6
Ins2k Ins2k Sk Ins3k SIk ∼ 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 1ck1 1 1c |
39 | 24, 38 | unex 4106 |
. . . . 5
Ins3k Sk k SIk 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 Ins2k Ins2k Sk Ins3k SIk ∼ 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 1ck1 1 1c |
40 | 39 | ins2kex 4307 |
. . . 4
Ins2k Ins3k Sk k SIk 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 Ins2k Ins2k Sk Ins3k SIk ∼ 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 1ck1 1 1c |
41 | 4, 40 | symdifex 4108 |
. . 3
Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk 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 Ins2k Ins2k Sk Ins3k SIk ∼ 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 1ck1 1 1c |
42 | 8 | pw1ex 4303 |
. . . 4
1 1 1
1c
|
43 | 42 | pw1ex 4303 |
. . 3
1 1 1 1
1c
|
44 | 41, 43 | imakex 4300 |
. 2
Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk 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 Ins2k Ins2k Sk Ins3k SIk ∼ 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 1ck1 1 1ck1 1 1 1 1c
|
45 | 44 | complex 4104 |
1
∼ Ins3k SIk SIk Sk Ins2k Ins3k Sk k SIk 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 Ins2k Ins2k Sk Ins3k SIk ∼ 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 1ck1 1 1ck1 1 1 1 1c
|