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