Proof of Theorem opexg
Step | Hyp | Ref
| Expression |
1 | | dfop2 4575 |
. 2
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 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 | | 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 | | imakexg 4299 |
. . . 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 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 k
|
19 | 17, 18 | mpan 651 |
. . 3
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 k
|
20 | | ssetkex 4294 |
. . . . . . . 8
Sk |
21 | 20 | ins2kex 4307 |
. . . . . . 7
Ins2k Sk |
22 | 17 | 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 |
23 | 22, 20 | 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
|
24 | | snex 4111 |
. . . . . . . . . 10
0c
|
25 | 24, 9 | xpkex 4289 |
. . . . . . . . 9
0c k
|
26 | 23, 25 | 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 |
27 | 26 | 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 |
28 | 21, 27 | 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 |
29 | 28, 5 | 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 |
30 | 29 | 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 |
31 | | imakexg 4299 |
. . . 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 ∼ 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 | 30, 31 | mpan 651 |
. . 3
∼ 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
|
33 | | unexg 4101 |
. . 3
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 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
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 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
|
34 | 19, 32, 33 | syl2an 463 |
. 2
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 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
|
35 | 1, 34 | syl5eqel 2437 |
1
|