Metamath Proof Explorer


Theorem foimacnv

Description: A reverse version of f1imacnv . (Contributed by Jeff Hankins, 16-Jul-2009)

Ref Expression
Assertion foimacnv F : A onto B C B F F -1 C = C

Proof

Step Hyp Ref Expression
1 resima F F -1 C F -1 C = F F -1 C
2 fofun F : A onto B Fun F
3 2 adantr F : A onto B C B Fun F
4 funcnvres2 Fun F F -1 C -1 = F F -1 C
5 3 4 syl F : A onto B C B F -1 C -1 = F F -1 C
6 5 imaeq1d F : A onto B C B F -1 C -1 F -1 C = F F -1 C F -1 C
7 resss F -1 C F -1
8 cnvss F -1 C F -1 F -1 C -1 F -1 -1
9 7 8 ax-mp F -1 C -1 F -1 -1
10 cnvcnvss F -1 -1 F
11 9 10 sstri F -1 C -1 F
12 funss F -1 C -1 F Fun F Fun F -1 C -1
13 11 2 12 mpsyl F : A onto B Fun F -1 C -1
14 13 adantr F : A onto B C B Fun F -1 C -1
15 df-ima F -1 C = ran F -1 C
16 df-rn ran F -1 C = dom F -1 C -1
17 15 16 eqtr2i dom F -1 C -1 = F -1 C
18 df-fn F -1 C -1 Fn F -1 C Fun F -1 C -1 dom F -1 C -1 = F -1 C
19 14 17 18 sylanblrc F : A onto B C B F -1 C -1 Fn F -1 C
20 dfdm4 dom F -1 C = ran F -1 C -1
21 forn F : A onto B ran F = B
22 21 sseq2d F : A onto B C ran F C B
23 22 biimpar F : A onto B C B C ran F
24 df-rn ran F = dom F -1
25 23 24 sseqtrdi F : A onto B C B C dom F -1
26 ssdmres C dom F -1 dom F -1 C = C
27 25 26 sylib F : A onto B C B dom F -1 C = C
28 20 27 eqtr3id F : A onto B C B ran F -1 C -1 = C
29 df-fo F -1 C -1 : F -1 C onto C F -1 C -1 Fn F -1 C ran F -1 C -1 = C
30 19 28 29 sylanbrc F : A onto B C B F -1 C -1 : F -1 C onto C
31 foima F -1 C -1 : F -1 C onto C F -1 C -1 F -1 C = C
32 30 31 syl F : A onto B C B F -1 C -1 F -1 C = C
33 6 32 eqtr3d F : A onto B C B F F -1 C F -1 C = C
34 1 33 eqtr3id F : A onto B C B F F -1 C = C