Step | Hyp | Ref
| Expression |
1 | | opkex 4113 |
. . . . 5
|
2 | 1 | elimak 4259 |
. . . 4
Ins2k Sk Ins3k SIk Sk k1 1 1c 1 1 1c
Ins2k Sk Ins3k SIk Sk |
3 | | elpw121c 4148 |
. . . . . . . 8
1 1 1c |
4 | 3 | anbi1i 676 |
. . . . . . 7
1 1
1c Ins2k Sk Ins3k SIk Sk
Ins2k Sk Ins3k SIk Sk |
5 | | 19.41v 1901 |
. . . . . . 7
Ins2k Sk Ins3k SIk Sk
Ins2k Sk Ins3k SIk Sk |
6 | 4, 5 | bitr4i 243 |
. . . . . 6
1 1
1c Ins2k Sk Ins3k SIk Sk
Ins2k Sk Ins3k SIk Sk |
7 | 6 | exbii 1582 |
. . . . 5
1 1 1c
Ins2k Sk Ins3k SIk Sk
Ins2k Sk Ins3k SIk Sk |
8 | | df-rex 2620 |
. . . . 5
1 1
1c Ins2k Sk Ins3k SIk Sk 1 1 1c
Ins2k Sk Ins3k SIk Sk |
9 | | excom 1741 |
. . . . 5
Ins2k Sk Ins3k SIk Sk
Ins2k Sk Ins3k SIk Sk |
10 | 7, 8, 9 | 3bitr4i 268 |
. . . 4
1 1
1c Ins2k Sk Ins3k SIk Sk
Ins2k Sk Ins3k SIk Sk |
11 | | snex 4111 |
. . . . . . 7
|
12 | | opkeq1 4059 |
. . . . . . . 8
|
13 | 12 | eleq1d 2419 |
. . . . . . 7
Ins2k Sk Ins3k SIk Sk Ins2k Sk Ins3k SIk Sk |
14 | 11, 13 | ceqsexv 2894 |
. . . . . 6
Ins2k Sk Ins3k SIk Sk
Ins2k Sk Ins3k SIk Sk |
15 | | elsymdif 3223 |
. . . . . 6
Ins2k Sk Ins3k SIk Sk
Ins2k Sk
Ins3k SIk Sk |
16 | | snex 4111 |
. . . . . . . . . 10
|
17 | | snex 4111 |
. . . . . . . . . 10
|
18 | | eqpwrelk.2 |
. . . . . . . . . 10
|
19 | 16, 17, 18 | otkelins2k 4255 |
. . . . . . . . 9
Ins2k Sk Sk |
20 | | vex 2862 |
. . . . . . . . . 10
|
21 | 20, 18 | elssetk 4270 |
. . . . . . . . 9
Sk |
22 | 19, 21 | bitri 240 |
. . . . . . . 8
Ins2k Sk |
23 | 16, 17, 18 | otkelins3k 4256 |
. . . . . . . . 9
Ins3k SIk Sk
SIk Sk |
24 | | eqpwrelk.1 |
. . . . . . . . . 10
|
25 | 20, 24 | opksnelsik 4265 |
. . . . . . . . 9
SIk Sk
Sk |
26 | | opkelssetkg 4268 |
. . . . . . . . . 10
Sk |
27 | 20, 24, 26 | mp2an 653 |
. . . . . . . . 9
Sk |
28 | 23, 25, 27 | 3bitri 262 |
. . . . . . . 8
Ins3k SIk Sk |
29 | 22, 28 | bibi12i 306 |
. . . . . . 7
Ins2k Sk
Ins3k SIk Sk |
30 | 29 | notbii 287 |
. . . . . 6
Ins2k Sk
Ins3k SIk Sk |
31 | 14, 15, 30 | 3bitri 262 |
. . . . 5
Ins2k Sk Ins3k SIk Sk
|
32 | 31 | exbii 1582 |
. . . 4
Ins2k Sk Ins3k SIk Sk
|
33 | 2, 10, 32 | 3bitri 262 |
. . 3
Ins2k Sk Ins3k SIk Sk k1 1 1c
|
34 | 33 | notbii 287 |
. 2
Ins2k Sk Ins3k SIk Sk k1 1 1c
|
35 | 1 | elcompl 3225 |
. 2
∼ Ins2k Sk Ins3k SIk Sk k1 1 1c
Ins2k Sk Ins3k SIk Sk k1 1 1c |
36 | | df-pw 3724 |
. . . 4
|
37 | 36 | eqeq2i 2363 |
. . 3
|
38 | | abeq2 2458 |
. . 3
|
39 | | alex 1572 |
. . 3
|
40 | 37, 38, 39 | 3bitri 262 |
. 2
|
41 | 34, 35, 40 | 3bitr4i 268 |
1
∼ Ins2k Sk Ins3k SIk Sk k1 1 1c |