Metamath Proof Explorer


Theorem foimacnv

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

Ref Expression
Assertion foimacnv ( ( 𝐹 : 𝐴onto𝐵𝐶𝐵 ) → ( 𝐹 “ ( 𝐹𝐶 ) ) = 𝐶 )

Proof

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