Metamath Proof Explorer


Theorem f1imacnv

Description: Preimage of an image. (Contributed by NM, 30-Sep-2004)

Ref Expression
Assertion f1imacnv ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( 𝐹 “ ( 𝐹𝐶 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 resima ( ( 𝐹 ↾ ( 𝐹𝐶 ) ) “ ( 𝐹𝐶 ) ) = ( 𝐹 “ ( 𝐹𝐶 ) )
2 df-f1 ( 𝐹 : 𝐴1-1𝐵 ↔ ( 𝐹 : 𝐴𝐵 ∧ Fun 𝐹 ) )
3 2 simprbi ( 𝐹 : 𝐴1-1𝐵 → Fun 𝐹 )
4 3 adantr ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → Fun 𝐹 )
5 funcnvres ( Fun 𝐹 ( 𝐹𝐶 ) = ( 𝐹 ↾ ( 𝐹𝐶 ) ) )
6 4 5 syl ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( 𝐹𝐶 ) = ( 𝐹 ↾ ( 𝐹𝐶 ) ) )
7 6 imaeq1d ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( ( 𝐹𝐶 ) “ ( 𝐹𝐶 ) ) = ( ( 𝐹 ↾ ( 𝐹𝐶 ) ) “ ( 𝐹𝐶 ) ) )
8 f1ores ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) )
9 f1ocnv ( ( 𝐹𝐶 ) : 𝐶1-1-onto→ ( 𝐹𝐶 ) → ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –1-1-onto𝐶 )
10 8 9 syl ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –1-1-onto𝐶 )
11 imadmrn ( ( 𝐹𝐶 ) “ dom ( 𝐹𝐶 ) ) = ran ( 𝐹𝐶 )
12 f1odm ( ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –1-1-onto𝐶 → dom ( 𝐹𝐶 ) = ( 𝐹𝐶 ) )
13 12 imaeq2d ( ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –1-1-onto𝐶 → ( ( 𝐹𝐶 ) “ dom ( 𝐹𝐶 ) ) = ( ( 𝐹𝐶 ) “ ( 𝐹𝐶 ) ) )
14 f1ofo ( ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –1-1-onto𝐶 ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –onto𝐶 )
15 forn ( ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –onto𝐶 → ran ( 𝐹𝐶 ) = 𝐶 )
16 14 15 syl ( ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –1-1-onto𝐶 → ran ( 𝐹𝐶 ) = 𝐶 )
17 11 13 16 3eqtr3a ( ( 𝐹𝐶 ) : ( 𝐹𝐶 ) –1-1-onto𝐶 → ( ( 𝐹𝐶 ) “ ( 𝐹𝐶 ) ) = 𝐶 )
18 10 17 syl ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( ( 𝐹𝐶 ) “ ( 𝐹𝐶 ) ) = 𝐶 )
19 7 18 eqtr3d ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( ( 𝐹 ↾ ( 𝐹𝐶 ) ) “ ( 𝐹𝐶 ) ) = 𝐶 )
20 1 19 eqtr3id ( ( 𝐹 : 𝐴1-1𝐵𝐶𝐴 ) → ( 𝐹 “ ( 𝐹𝐶 ) ) = 𝐶 )