Step | Hyp | Ref
| Expression |
1 | | sikexlem.1 |
. . 3
1c k 1c |
2 | | sikexlem.2 |
. . 3
1c k 1c |
3 | | ssofeq 4077 |
. . 3
1c
k
1c
1c k 1c
1c k
1c |
4 | 1, 2, 3 | mp2an 653 |
. 2
1c k 1c
|
5 | | df-ral 2619 |
. . 3
1c
k
1c 1c k 1c
|
6 | | elxpk 4196 |
. . . . . . . 8
1c k 1c 1c
1c |
7 | | el1c 4139 |
. . . . . . . . . . . . . 14
1c
|
8 | | el1c 4139 |
. . . . . . . . . . . . . 14
1c
|
9 | 7, 8 | anbi12i 678 |
. . . . . . . . . . . . 13
1c 1c
|
10 | | eeanv 1913 |
. . . . . . . . . . . . 13
|
11 | 9, 10 | bitr4i 243 |
. . . . . . . . . . . 12
1c 1c |
12 | 11 | anbi2i 675 |
. . . . . . . . . . 11
1c
1c |
13 | | df-3an 936 |
. . . . . . . . . . . . . 14
|
14 | | ancom 437 |
. . . . . . . . . . . . . 14
|
15 | 13, 14 | bitri 240 |
. . . . . . . . . . . . 13
|
16 | 15 | 2exbii 1583 |
. . . . . . . . . . . 12
|
17 | | 19.42vv 1907 |
. . . . . . . . . . . 12
|
18 | 16, 17 | bitri 240 |
. . . . . . . . . . 11
|
19 | 12, 18 | bitr4i 243 |
. . . . . . . . . 10
1c
1c
|
20 | 19 | 2exbii 1583 |
. . . . . . . . 9
1c
1c |
21 | | exrot4 1745 |
. . . . . . . . 9
|
22 | 20, 21 | bitr4i 243 |
. . . . . . . 8
1c
1c |
23 | | snex 4111 |
. . . . . . . . . 10
|
24 | | snex 4111 |
. . . . . . . . . 10
|
25 | | opkeq1 4059 |
. . . . . . . . . . 11
|
26 | 25 | eqeq2d 2364 |
. . . . . . . . . 10
|
27 | | opkeq2 4060 |
. . . . . . . . . . 11
|
28 | 27 | eqeq2d 2364 |
. . . . . . . . . 10
|
29 | 23, 24, 26, 28 | ceqsex2v 2896 |
. . . . . . . . 9
|
30 | 29 | 2exbii 1583 |
. . . . . . . 8
|
31 | 6, 22, 30 | 3bitri 262 |
. . . . . . 7
1c k 1c |
32 | 31 | imbi1i 315 |
. . . . . 6
1c k
1c
|
33 | | 19.23vv 1892 |
. . . . . 6
|
34 | 32, 33 | bitr4i 243 |
. . . . 5
1c k
1c
|
35 | 34 | albii 1566 |
. . . 4
1c k 1c
|
36 | | alrot3 1738 |
. . . 4
|
37 | 35, 36 | bitri 240 |
. . 3
1c k 1c
|
38 | | opkex 4113 |
. . . . 5
|
39 | | eleq1 2413 |
. . . . . 6
|
40 | | eleq1 2413 |
. . . . . 6
|
41 | 39, 40 | bibi12d 312 |
. . . . 5
|
42 | 38, 41 | ceqsalv 2885 |
. . . 4
|
43 | 42 | 2albii 1567 |
. . 3
|
44 | 5, 37, 43 | 3bitri 262 |
. 2
1c
k
1c |
45 | 4, 44 | bitri 240 |
1
|