Step | Hyp | Ref
| Expression |
1 | | nfmpt1 4747 |
. . . . . . 7
|
2 | | ofpreima.1 |
. . . . . . 7
|
3 | | ofpreima.2 |
. . . . . . 7
|
4 | | ofpreima.3 |
. . . . . . 7
|
5 | | eqidd 2623 |
. . . . . . 7
|
6 | | ofpreima.4 |
. . . . . . . 8
|
7 | | fnov 6768 |
. . . . . . . 8
|
8 | 6, 7 | sylib 208 |
. . . . . . 7
|
9 | 1, 2, 3, 4, 5, 8 | ofoprabco 29464 |
. . . . . 6
|
10 | 9 | cnveqd 5298 |
. . . . 5
|
11 | | cnvco 5308 |
. . . . 5
|
12 | 10, 11 | syl6eq 2672 |
. . . 4
|
13 | 12 | imaeq1d 5465 |
. . 3
|
14 | | imaco 5640 |
. . 3
|
15 | 13, 14 | syl6eq 2672 |
. 2
|
16 | | dfima2 5468 |
. . 3
|
17 | | vex 3203 |
. . . . . . . 8
|
18 | | vex 3203 |
. . . . . . . 8
|
19 | 17, 18 | brcnv 5305 |
. . . . . . 7
|
20 | | funmpt 5926 |
. . . . . . . . 9
|
21 | | funbrfv2b 6240 |
. . . . . . . . 9
|
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
|
23 | | opex 4932 |
. . . . . . . . . . 11
|
24 | | eqid 2622 |
. . . . . . . . . . 11
|
25 | 23, 24 | dmmpti 6023 |
. . . . . . . . . 10
|
26 | 25 | eleq2i 2693 |
. . . . . . . . 9
|
27 | 26 | anbi1i 731 |
. . . . . . . 8
|
28 | 22, 27 | bitri 264 |
. . . . . . 7
|
29 | | fveq2 6191 |
. . . . . . . . . . 11
|
30 | | fveq2 6191 |
. . . . . . . . . . 11
|
31 | 29, 30 | opeq12d 4410 |
. . . . . . . . . 10
|
32 | | opex 4932 |
. . . . . . . . . 10
|
33 | 31, 24, 32 | fvmpt 6282 |
. . . . . . . . 9
|
34 | 33 | eqeq1d 2624 |
. . . . . . . 8
|
35 | 34 | pm5.32i 669 |
. . . . . . 7
|
36 | 19, 28, 35 | 3bitri 286 |
. . . . . 6
|
37 | 36 | rexbii 3041 |
. . . . 5
|
38 | 37 | abbii 2739 |
. . . 4
|
39 | | nfv 1843 |
. . . . 5
|
40 | | nfab1 2766 |
. . . . 5
|
41 | | nfcv 2764 |
. . . . 5
|
42 | | eliun 4524 |
. . . . . 6
|
43 | | ffn 6045 |
. . . . . . . . . . . . 13
|
44 | | fniniseg 6338 |
. . . . . . . . . . . . 13
|
45 | 2, 43, 44 | 3syl 18 |
. . . . . . . . . . . 12
|
46 | | ffn 6045 |
. . . . . . . . . . . . 13
|
47 | | fniniseg 6338 |
. . . . . . . . . . . . 13
|
48 | 3, 46, 47 | 3syl 18 |
. . . . . . . . . . . 12
|
49 | 45, 48 | anbi12d 747 |
. . . . . . . . . . 11
|
50 | | elin 3796 |
. . . . . . . . . . 11
|
51 | | anandi 871 |
. . . . . . . . . . 11
|
52 | 49, 50, 51 | 3bitr4g 303 |
. . . . . . . . . 10
|
53 | 52 | adantr 481 |
. . . . . . . . 9
|
54 | | cnvimass 5485 |
. . . . . . . . . . . . . 14
|
55 | | fndm 5990 |
. . . . . . . . . . . . . . 15
|
56 | 6, 55 | syl 17 |
. . . . . . . . . . . . . 14
|
57 | 54, 56 | syl5sseq 3653 |
. . . . . . . . . . . . 13
|
58 | 57 | sselda 3603 |
. . . . . . . . . . . 12
|
59 | | 1st2nd2 7205 |
. . . . . . . . . . . 12
|
60 | | eqeq2 2633 |
. . . . . . . . . . . 12
|
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . 11
|
62 | | fvex 6201 |
. . . . . . . . . . . 12
|
63 | | fvex 6201 |
. . . . . . . . . . . 12
|
64 | 62, 63 | opth 4945 |
. . . . . . . . . . 11
|
65 | 61, 64 | syl6bb 276 |
. . . . . . . . . 10
|
66 | 65 | anbi2d 740 |
. . . . . . . . 9
|
67 | 53, 66 | bitr4d 271 |
. . . . . . . 8
|
68 | 67 | rexbidva 3049 |
. . . . . . 7
|
69 | | abid 2610 |
. . . . . . 7
|
70 | 68, 69 | syl6bbr 278 |
. . . . . 6
|
71 | 42, 70 | syl5rbb 273 |
. . . . 5
|
72 | 39, 40, 41, 71 | eqrd 3622 |
. . . 4
|
73 | 38, 72 | syl5eq 2668 |
. . 3
|
74 | 16, 73 | syl5eq 2668 |
. 2
|
75 | 15, 74 | eqtrd 2656 |
1
|