Proof of Theorem srelkex
Step | Hyp | Ref
| Expression |
1 | | nncex 4396 |
. . 3
Nn ![_V](rmcv.gif) |
2 | 1, 1 | xpkex 4289 |
. 2
Nn k Nn ![_V](rmcv.gif) |
3 | | 1cex 4142 |
. . . . . . . . . . . 12
1c
![_V](rmcv.gif) |
4 | 3 | pwex 4329 |
. . . . . . . . . . 11
1c
![_V](rmcv.gif) |
5 | | vvex 4109 |
. . . . . . . . . . 11
![_V](rmcv.gif) |
6 | 4, 5 | xpkex 4289 |
. . . . . . . . . 10
![(](lp.gif) 1c k ![_V](rmcv.gif)
![_V](rmcv.gif) |
7 | | ssetkex 4294 |
. . . . . . . . . . . . 13
Sk ![_V](rmcv.gif) |
8 | 7 | ins3kex 4308 |
. . . . . . . . . . . 12
Ins3k Sk ![_V](rmcv.gif) |
9 | 7 | sikex 4297 |
. . . . . . . . . . . . 13
SIk Sk ![_V](rmcv.gif) |
10 | 9 | ins2kex 4307 |
. . . . . . . . . . . 12
Ins2k SIk Sk ![_V](rmcv.gif) |
11 | 8, 10 | symdifex 4108 |
. . . . . . . . . . 11
Ins3k Sk Ins2k SIk Sk
![_V](rmcv.gif) |
12 | 3 | pw1ex 4303 |
. . . . . . . . . . . . 13
1
1c
![_V](rmcv.gif) |
13 | 12 | pw1ex 4303 |
. . . . . . . . . . . 12
1 1
1c
![_V](rmcv.gif) |
14 | 13 | pw1ex 4303 |
. . . . . . . . . . 11
1 1 1
1c
![_V](rmcv.gif) |
15 | 11, 14 | imakex 4300 |
. . . . . . . . . 10
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c
![_V](rmcv.gif) |
16 | 6, 15 | difex 4107 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
17 | 16 | sikex 4297 |
. . . . . . . 8
SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
18 | 17 | ins3kex 4308 |
. . . . . . 7
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
19 | 7 | ins2kex 4307 |
. . . . . . 7
Ins2k Sk ![_V](rmcv.gif) |
20 | 18, 19 | inex 4105 |
. . . . . 6
Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk
![_V](rmcv.gif) |
21 | 20, 13 | imakex 4300 |
. . . . 5
![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
22 | 21 | ins3kex 4308 |
. . . 4
Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
23 | 11, 13 | imakex 4300 |
. . . . . . . . . 10
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
24 | 23 | complex 4104 |
. . . . . . . . 9
∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
25 | 24 | sikex 4297 |
. . . . . . . 8
SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
26 | 25 | ins3kex 4308 |
. . . . . . 7
Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
27 | 26, 19 | inex 4105 |
. . . . . 6
Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk
![_V](rmcv.gif) |
28 | 27, 13 | imakex 4300 |
. . . . 5
![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
29 | 28 | ins2kex 4307 |
. . . 4
Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) |
30 | 22, 29 | inex 4105 |
. . 3
Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
31 | 30, 14 | imakex 4300 |
. 2
![(](lp.gif) Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c
![_V](rmcv.gif) |
32 | 2, 31 | inex 4105 |
1
![(](lp.gif) Nn k Nn ![(](lp.gif) Ins3k ![(](lp.gif) Ins3k SIk ![(](lp.gif) ![(](lp.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
Ins2k Sk ![)](rp.gif) k 1 1 1c Ins2k ![(](lp.gif) Ins3k SIk ∼ ![(](lp.gif) Ins3k Sk Ins2k SIk Sk ![)](rp.gif) k 1 1 1c Ins2k Sk ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |