Step | Hyp | Ref
| Expression |
1 | | unab 3521 |
. . 3
Nn fin fin Nn fin
fin |
2 | | df-sn 3741 |
. . . . . 6
|
3 | | elun 3220 |
. . . . . . . . . 10
k fin k k fin k
|
4 | | vex 2862 |
. . . . . . . . . . . . . 14
|
5 | 4 | elimak 4259 |
. . . . . . . . . . . . 13
k fin k
k fin |
6 | | vex 2862 |
. . . . . . . . . . . . . 14
|
7 | | opkeq1 4059 |
. . . . . . . . . . . . . . 15
|
8 | 7 | eleq1d 2419 |
. . . . . . . . . . . . . 14
k fin k fin |
9 | 6, 8 | rexsn 3768 |
. . . . . . . . . . . . 13
k fin k fin |
10 | 5, 9 | bitri 240 |
. . . . . . . . . . . 12
k fin k k fin |
11 | 6, 4 | opkelcnvk 4250 |
. . . . . . . . . . . 12
k fin fin |
12 | 10, 11 | bitri 240 |
. . . . . . . . . . 11
k fin k fin |
13 | 4 | elsnc 3756 |
. . . . . . . . . . 11
|
14 | 12, 13 | orbi12i 507 |
. . . . . . . . . 10
k fin k
fin
|
15 | 3, 14 | bitri 240 |
. . . . . . . . 9
k fin k fin
|
16 | 4 | elimak 4259 |
. . . . . . . . . 10
fin k
fin |
17 | 7 | eleq1d 2419 |
. . . . . . . . . . 11
fin fin |
18 | 6, 17 | rexsn 3768 |
. . . . . . . . . 10
fin fin |
19 | 16, 18 | bitri 240 |
. . . . . . . . 9
fin k fin |
20 | 15, 19 | orbi12i 507 |
. . . . . . . 8
k fin k
fin k fin fin |
21 | | elun 3220 |
. . . . . . . 8
k fin k
fin k k fin k
fin k |
22 | | df-3or 935 |
. . . . . . . 8
fin fin fin
fin |
23 | 20, 21, 22 | 3bitr4i 268 |
. . . . . . 7
k fin k
fin k fin fin |
24 | 23 | abbi2i 2464 |
. . . . . 6
k fin k
fin k
fin fin |
25 | 2, 24 | uneq12i 3416 |
. . . . 5
k fin k
fin k
fin
fin |
26 | | unab 3521 |
. . . . 5
fin fin
fin fin |
27 | 25, 26 | eqtri 2373 |
. . . 4
k fin k
fin k
fin
fin |
28 | 27 | uneq2i 3415 |
. . 3
Nn k fin k
fin k
Nn
fin fin |
29 | | imor 401 |
. . . . 5
Nn fin
fin Nn
fin fin |
30 | | df-ne 2518 |
. . . . . . . 8
|
31 | 30 | imbi1i 315 |
. . . . . . 7
fin fin fin fin |
32 | | df-or 359 |
. . . . . . 7
fin fin fin fin |
33 | 31, 32 | bitr4i 243 |
. . . . . 6
fin fin
fin fin |
34 | 33 | orbi2i 505 |
. . . . 5
Nn fin
fin Nn
fin fin |
35 | 29, 34 | bitri 240 |
. . . 4
Nn fin
fin Nn
fin fin |
36 | 35 | abbii 2465 |
. . 3
Nn fin
fin
Nn fin fin |
37 | 1, 28, 36 | 3eqtr4i 2383 |
. 2
Nn k fin k
fin k
Nn
fin fin |
38 | | abexv 4324 |
. . 3
Nn |
39 | | snex 4111 |
. . . 4
|
40 | | ltfinex 4464 |
. . . . . . . 8
fin |
41 | 40 | cnvkex 4287 |
. . . . . . 7
k fin |
42 | | snex 4111 |
. . . . . . 7
|
43 | 41, 42 | imakex 4300 |
. . . . . 6
k fin k |
44 | 43, 42 | unex 4106 |
. . . . 5
k fin k |
45 | 40, 42 | imakex 4300 |
. . . . 5
fin k |
46 | 44, 45 | unex 4106 |
. . . 4
k fin k
fin k
|
47 | 39, 46 | unex 4106 |
. . 3
k fin k
fin k
|
48 | 38, 47 | unex 4106 |
. 2
Nn k fin k
fin k |
49 | 37, 48 | eqeltrri 2424 |
1
Nn fin
fin |