Description: Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015) (Proof shortened by Wolf Lammen, 29-May-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | f1eqcocnv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1cocnv1 | |
|
2 | coeq2 | |
|
3 | 2 | eqeq1d | |
4 | 1 3 | syl5ibcom | |
5 | 4 | adantr | |
6 | f1fn | |
|
7 | 6 | adantl | |
8 | 7 | adantr | |
9 | f1fn | |
|
10 | 9 | adantr | |
11 | 10 | adantr | |
12 | equid | |
|
13 | resieq | |
|
14 | 12 13 | mpbiri | |
15 | 14 | anidms | |
16 | 15 | adantl | |
17 | breq | |
|
18 | 17 | ad2antlr | |
19 | 16 18 | mpbird | |
20 | fnfun | |
|
21 | 7 20 | syl | |
22 | 7 | fndmd | |
23 | 22 | eleq2d | |
24 | 23 | biimpar | |
25 | funopfvb | |
|
26 | 21 24 25 | syl2an2r | |
27 | 26 | bicomd | |
28 | df-br | |
|
29 | eqcom | |
|
30 | 27 28 29 | 3bitr4g | |
31 | 30 | biimpd | |
32 | df-br | |
|
33 | fnfun | |
|
34 | 10 33 | syl | |
35 | 10 | fndmd | |
36 | 35 | eleq2d | |
37 | 36 | biimpar | |
38 | funopfvb | |
|
39 | 34 37 38 | syl2an2r | |
40 | 32 39 | bitr4id | |
41 | vex | |
|
42 | vex | |
|
43 | 41 42 | brcnv | |
44 | eqcom | |
|
45 | 40 43 44 | 3bitr4g | |
46 | 45 | biimpd | |
47 | 31 46 | anim12d | |
48 | 47 | eximdv | |
49 | 42 42 | brco | |
50 | fvex | |
|
51 | 50 | eqvinc | |
52 | 48 49 51 | 3imtr4g | |
53 | 52 | adantlr | |
54 | 19 53 | mpd | |
55 | 8 11 54 | eqfnfvd | |
56 | 55 | eqcomd | |
57 | 56 | ex | |
58 | 5 57 | impbid | |