Metamath Proof Explorer


Theorem f1eqcocnvOLD

Description: Obsolete version of f1eqcocnv as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion f1eqcocnvOLD 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 fndm GFnAdomG=A
23 7 22 syl F:A1-1BG:A1-1BdomG=A
24 23 eleq2d F:A1-1BG:A1-1BxdomGxA
25 24 biimpar F:A1-1BG:A1-1BxAxdomG
26 funopfvb FunGxdomGGx=yxyG
27 21 25 26 syl2an2r F:A1-1BG:A1-1BxAGx=yxyG
28 27 bicomd F:A1-1BG:A1-1BxAxyGGx=y
29 df-br xGyxyG
30 eqcom y=GxGx=y
31 28 29 30 3bitr4g F:A1-1BG:A1-1BxAxGyy=Gx
32 31 biimpd F:A1-1BG:A1-1BxAxGyy=Gx
33 df-br xFyxyF
34 fnfun FFnAFunF
35 10 34 syl F:A1-1BG:A1-1BFunF
36 fndm FFnAdomF=A
37 10 36 syl F:A1-1BG:A1-1BdomF=A
38 37 eleq2d F:A1-1BG:A1-1BxdomFxA
39 38 biimpar F:A1-1BG:A1-1BxAxdomF
40 funopfvb FunFxdomFFx=yxyF
41 35 39 40 syl2an2r F:A1-1BG:A1-1BxAFx=yxyF
42 33 41 bitr4id F:A1-1BG:A1-1BxAxFyFx=y
43 vex yV
44 vex xV
45 43 44 brcnv yF-1xxFy
46 eqcom y=FxFx=y
47 42 45 46 3bitr4g F:A1-1BG:A1-1BxAyF-1xy=Fx
48 47 biimpd F:A1-1BG:A1-1BxAyF-1xy=Fx
49 32 48 anim12d F:A1-1BG:A1-1BxAxGyyF-1xy=Gxy=Fx
50 49 eximdv F:A1-1BG:A1-1BxAyxGyyF-1xyy=Gxy=Fx
51 44 44 brco xF-1GxyxGyyF-1x
52 fvex GxV
53 52 eqvinc Gx=Fxyy=Gxy=Fx
54 50 51 53 3imtr4g F:A1-1BG:A1-1BxAxF-1GxGx=Fx
55 54 adantlr F:A1-1BG:A1-1BF-1G=IAxAxF-1GxGx=Fx
56 19 55 mpd F:A1-1BG:A1-1BF-1G=IAxAGx=Fx
57 8 11 56 eqfnfvd F:A1-1BG:A1-1BF-1G=IAG=F
58 57 eqcomd F:A1-1BG:A1-1BF-1G=IAF=G
59 58 ex F:A1-1BG:A1-1BF-1G=IAF=G
60 5 59 impbid F:A1-1BG:A1-1BF=GF-1G=IA