Metamath Proof Explorer


Theorem f1eqcocnv

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 F:A1-1BG:A1-1BF=GF-1G=IA

Proof

Step Hyp Ref Expression
1 f1cocnv1 F:A1-1BF-1F=IA
2 coeq2 F=GF-1F=F-1G
3 2 eqeq1d F=GF-1F=IAF-1G=IA
4 1 3 syl5ibcom F:A1-1BF=GF-1G=IA
5 4 adantr F:A1-1BG:A1-1BF=GF-1G=IA
6 f1fn G:A1-1BGFnA
7 6 adantl F:A1-1BG:A1-1BGFnA
8 7 adantr F:A1-1BG:A1-1BF-1G=IAGFnA
9 f1fn F:A1-1BFFnA
10 9 adantr F:A1-1BG:A1-1BFFnA
11 10 adantr F:A1-1BG:A1-1BF-1G=IAFFnA
12 equid x=x
13 resieq xAxAxIAxx=x
14 12 13 mpbiri xAxAxIAx
15 14 anidms xAxIAx
16 15 adantl F:A1-1BG:A1-1BF-1G=IAxAxIAx
17 breq F-1G=IAxF-1GxxIAx
18 17 ad2antlr F:A1-1BG:A1-1BF-1G=IAxAxF-1GxxIAx
19 16 18 mpbird F:A1-1BG:A1-1BF-1G=IAxAxF-1Gx
20 fnfun GFnAFunG
21 7 20 syl F:A1-1BG:A1-1BFunG
22 7 fndmd F:A1-1BG:A1-1BdomG=A
23 22 eleq2d F:A1-1BG:A1-1BxdomGxA
24 23 biimpar F:A1-1BG:A1-1BxAxdomG
25 funopfvb FunGxdomGGx=yxyG
26 21 24 25 syl2an2r F:A1-1BG:A1-1BxAGx=yxyG
27 26 bicomd F:A1-1BG:A1-1BxAxyGGx=y
28 df-br xGyxyG
29 eqcom y=GxGx=y
30 27 28 29 3bitr4g F:A1-1BG:A1-1BxAxGyy=Gx
31 30 biimpd F:A1-1BG:A1-1BxAxGyy=Gx
32 df-br xFyxyF
33 fnfun FFnAFunF
34 10 33 syl F:A1-1BG:A1-1BFunF
35 10 fndmd F:A1-1BG:A1-1BdomF=A
36 35 eleq2d F:A1-1BG:A1-1BxdomFxA
37 36 biimpar F:A1-1BG:A1-1BxAxdomF
38 funopfvb FunFxdomFFx=yxyF
39 34 37 38 syl2an2r F:A1-1BG:A1-1BxAFx=yxyF
40 32 39 bitr4id F:A1-1BG:A1-1BxAxFyFx=y
41 vex yV
42 vex xV
43 41 42 brcnv yF-1xxFy
44 eqcom y=FxFx=y
45 40 43 44 3bitr4g F:A1-1BG:A1-1BxAyF-1xy=Fx
46 45 biimpd F:A1-1BG:A1-1BxAyF-1xy=Fx
47 31 46 anim12d F:A1-1BG:A1-1BxAxGyyF-1xy=Gxy=Fx
48 47 eximdv F:A1-1BG:A1-1BxAyxGyyF-1xyy=Gxy=Fx
49 42 42 brco xF-1GxyxGyyF-1x
50 fvex GxV
51 50 eqvinc Gx=Fxyy=Gxy=Fx
52 48 49 51 3imtr4g F:A1-1BG:A1-1BxAxF-1GxGx=Fx
53 52 adantlr F:A1-1BG:A1-1BF-1G=IAxAxF-1GxGx=Fx
54 19 53 mpd F:A1-1BG:A1-1BF-1G=IAxAGx=Fx
55 8 11 54 eqfnfvd F:A1-1BG:A1-1BF-1G=IAG=F
56 55 eqcomd F:A1-1BG:A1-1BF-1G=IAF=G
57 56 ex F:A1-1BG:A1-1BF-1G=IAF=G
58 5 57 impbid F:A1-1BG:A1-1BF=GF-1G=IA