Proof of Theorem imagekexg
Step | Hyp | Ref
| Expression |
1 | | df-imagek 4194 |
. 2
Imagek ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif)
![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif) ![)](rp.gif) |
2 | | sikexg 4296 |
. . . . . . . 8
![(](lp.gif) SIk ![_V](rmcv.gif) ![)](rp.gif) |
3 | | cnvkexg 4286 |
. . . . . . . 8
SIk k SIk ![_V](rmcv.gif) ![)](rp.gif) |
4 | 2, 3 | syl 15 |
. . . . . . 7
![(](lp.gif) k SIk ![_V](rmcv.gif) ![)](rp.gif) |
5 | | ssetkex 4294 |
. . . . . . . 8
Sk ![_V](rmcv.gif) |
6 | | cokexg 4309 |
. . . . . . . 8
![(](lp.gif) Sk k SIk ![_V](rmcv.gif) Sk k k
SIk ![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
7 | 5, 6 | mpan 651 |
. . . . . . 7
![(](lp.gif) k SIk Sk k k SIk ![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
8 | 4, 7 | syl 15 |
. . . . . 6
![(](lp.gif) Sk k k SIk ![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
9 | | ins3kexg 4306 |
. . . . . 6
![(](lp.gif) Sk k k SIk ![A](_ca.gif) Ins3k Sk k k SIk ![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
10 | 8, 9 | syl 15 |
. . . . 5
![(](lp.gif) Ins3k Sk k k SIk ![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
11 | 5 | ins2kex 4307 |
. . . . . 6
Ins2k Sk ![_V](rmcv.gif) |
12 | | symdifexg 4103 |
. . . . . 6
![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![_V](rmcv.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![_V](rmcv.gif) ![)](rp.gif) |
13 | 11, 12 | mpan 651 |
. . . . 5
Ins3k Sk k k SIk ![A](_ca.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![_V](rmcv.gif) ![)](rp.gif) |
14 | 10, 13 | syl 15 |
. . . 4
![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![_V](rmcv.gif) ![)](rp.gif) |
15 | | 1cex 4142 |
. . . . . . 7
1c
![_V](rmcv.gif) |
16 | 15 | pw1ex 4303 |
. . . . . 6
1
1c
![_V](rmcv.gif) |
17 | 16 | pw1ex 4303 |
. . . . 5
1 1
1c
![_V](rmcv.gif) |
18 | | imakexg 4299 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) 1 1 1c ![_V](rmcv.gif)
![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) ![)](rp.gif) |
19 | 17, 18 | mpan2 652 |
. . . 4
![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) ![)](rp.gif) |
20 | 14, 19 | syl 15 |
. . 3
![(](lp.gif) ![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) ![)](rp.gif) |
21 | | vvex 4109 |
. . . . 5
![_V](rmcv.gif) |
22 | 21, 21 | xpkex 4289 |
. . . 4
![(](lp.gif) k ![_V](rmcv.gif)
![_V](rmcv.gif) |
23 | | difexg 4102 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c
![_V](rmcv.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif)
![_V](rmcv.gif) ![)](rp.gif) |
24 | 22, 23 | mpan 651 |
. . 3
![(](lp.gif) ![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c
![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif)
![_V](rmcv.gif) ![)](rp.gif) |
25 | 20, 24 | syl 15 |
. 2
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif)
![(](lp.gif) Ins2k Sk Ins3k Sk k k SIk ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) k 1 1 1c![)](rp.gif)
![_V](rmcv.gif) ![)](rp.gif) |
26 | 1, 25 | syl5eqel 2437 |
1
![(](lp.gif)
Imagek ![_V](rmcv.gif) ![)](rp.gif) |