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