Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. 2
|
2 | | f1of1 5413 |
. . 3
|
3 | | df-br 3966 |
. . . . 5
|
4 | | eleq2 2221 |
. . . . . . 7
|
5 | | f1fn 5377 |
. . . . . . . . 9
|
6 | | funfvex 5485 |
. . . . . . . . . . . 12
|
7 | 6 | funfni 5270 |
. . . . . . . . . . 11
|
8 | | funfvex 5485 |
. . . . . . . . . . . 12
|
9 | 8 | funfni 5270 |
. . . . . . . . . . 11
|
10 | 7, 9 | anim12dan 590 |
. . . . . . . . . 10
|
11 | | eqeq1 2164 |
. . . . . . . . . . . . . 14
|
12 | 11 | anbi1d 461 |
. . . . . . . . . . . . 13
|
13 | 12 | anbi1d 461 |
. . . . . . . . . . . 12
|
14 | 13 | 2rexbidv 2482 |
. . . . . . . . . . 11
|
15 | | eqeq1 2164 |
. . . . . . . . . . . . . 14
|
16 | 15 | anbi2d 460 |
. . . . . . . . . . . . 13
|
17 | 16 | anbi1d 461 |
. . . . . . . . . . . 12
|
18 | 17 | 2rexbidv 2482 |
. . . . . . . . . . 11
|
19 | 14, 18 | opelopabg 4228 |
. . . . . . . . . 10
|
20 | 10, 19 | syl 14 |
. . . . . . . . 9
|
21 | 5, 20 | sylan 281 |
. . . . . . . 8
|
22 | | anass 399 |
. . . . . . . . . . . . . . 15
|
23 | | f1fveq 5722 |
. . . . . . . . . . . . . . . . . 18
|
24 | | equcom 1686 |
. . . . . . . . . . . . . . . . . 18
|
25 | 23, 24 | bitrdi 195 |
. . . . . . . . . . . . . . . . 17
|
26 | 25 | anassrs 398 |
. . . . . . . . . . . . . . . 16
|
27 | 26 | anbi1d 461 |
. . . . . . . . . . . . . . 15
|
28 | 22, 27 | syl5bb 191 |
. . . . . . . . . . . . . 14
|
29 | 28 | rexbidv 2458 |
. . . . . . . . . . . . 13
|
30 | | r19.42v 2614 |
. . . . . . . . . . . . 13
|
31 | 29, 30 | bitrdi 195 |
. . . . . . . . . . . 12
|
32 | 31 | rexbidva 2454 |
. . . . . . . . . . 11
|
33 | | breq1 3968 |
. . . . . . . . . . . . . . 15
|
34 | 33 | anbi2d 460 |
. . . . . . . . . . . . . 14
|
35 | 34 | rexbidv 2458 |
. . . . . . . . . . . . 13
|
36 | 35 | ceqsrexv 2842 |
. . . . . . . . . . . 12
|
37 | 36 | adantl 275 |
. . . . . . . . . . 11
|
38 | 32, 37 | bitrd 187 |
. . . . . . . . . 10
|
39 | | f1fveq 5722 |
. . . . . . . . . . . . . . 15
|
40 | | equcom 1686 |
. . . . . . . . . . . . . . 15
|
41 | 39, 40 | bitrdi 195 |
. . . . . . . . . . . . . 14
|
42 | 41 | anassrs 398 |
. . . . . . . . . . . . 13
|
43 | 42 | anbi1d 461 |
. . . . . . . . . . . 12
|
44 | 43 | rexbidva 2454 |
. . . . . . . . . . 11
|
45 | | breq2 3969 |
. . . . . . . . . . . . 13
|
46 | 45 | ceqsrexv 2842 |
. . . . . . . . . . . 12
|
47 | 46 | adantl 275 |
. . . . . . . . . . 11
|
48 | 44, 47 | bitrd 187 |
. . . . . . . . . 10
|
49 | 38, 48 | sylan9bb 458 |
. . . . . . . . 9
|
50 | 49 | anandis 582 |
. . . . . . . 8
|
51 | 21, 50 | bitrd 187 |
. . . . . . 7
|
52 | 4, 51 | sylan9bbr 459 |
. . . . . 6
|
53 | 52 | an32s 558 |
. . . . 5
|
54 | 3, 53 | syl5rbb 192 |
. . . 4
|
55 | 54 | ralrimivva 2539 |
. . 3
|
56 | 2, 55 | sylan 281 |
. 2
|
57 | | df-isom 5179 |
. 2
|
58 | 1, 56, 57 | sylanbrc 414 |
1
|