# Metamath Proof Explorer

## Theorem f1imacnv

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

Ref Expression
Assertion f1imacnv ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to {{F}}^{-1}\left[{F}\left[{C}\right]\right]={C}$

### Proof

Step Hyp Ref Expression
1 resima ${⊢}\left({{{F}}^{-1}↾}_{{F}\left[{C}\right]}\right)\left[{F}\left[{C}\right]\right]={{F}}^{-1}\left[{F}\left[{C}\right]\right]$
2 df-f1 ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
3 2 simprbi ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to \mathrm{Fun}{{F}}^{-1}$
4 3 adantr ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \mathrm{Fun}{{F}}^{-1}$
5 funcnvres ${⊢}\mathrm{Fun}{{F}}^{-1}\to {\left({{F}↾}_{{C}}\right)}^{-1}={{{F}}^{-1}↾}_{{F}\left[{C}\right]}$
6 4 5 syl ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to {\left({{F}↾}_{{C}}\right)}^{-1}={{{F}}^{-1}↾}_{{F}\left[{C}\right]}$
7 6 imaeq1d ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to {\left({{F}↾}_{{C}}\right)}^{-1}\left[{F}\left[{C}\right]\right]=\left({{{F}}^{-1}↾}_{{F}\left[{C}\right]}\right)\left[{F}\left[{C}\right]\right]$
8 f1ores ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \left({{F}↾}_{{C}}\right):{C}\underset{1-1 onto}{⟶}{F}\left[{C}\right]$
9 f1ocnv ${⊢}\left({{F}↾}_{{C}}\right):{C}\underset{1-1 onto}{⟶}{F}\left[{C}\right]\to {\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{1-1 onto}{⟶}{C}$
10 8 9 syl ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to {\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{1-1 onto}{⟶}{C}$
11 imadmrn ${⊢}{\left({{F}↾}_{{C}}\right)}^{-1}\left[\mathrm{dom}{\left({{F}↾}_{{C}}\right)}^{-1}\right]=\mathrm{ran}{\left({{F}↾}_{{C}}\right)}^{-1}$
12 f1odm ${⊢}{\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{1-1 onto}{⟶}{C}\to \mathrm{dom}{\left({{F}↾}_{{C}}\right)}^{-1}={F}\left[{C}\right]$
13 12 imaeq2d ${⊢}{\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{1-1 onto}{⟶}{C}\to {\left({{F}↾}_{{C}}\right)}^{-1}\left[\mathrm{dom}{\left({{F}↾}_{{C}}\right)}^{-1}\right]={\left({{F}↾}_{{C}}\right)}^{-1}\left[{F}\left[{C}\right]\right]$
14 f1ofo ${⊢}{\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{1-1 onto}{⟶}{C}\to {\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{onto}{⟶}{C}$
15 forn ${⊢}{\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{onto}{⟶}{C}\to \mathrm{ran}{\left({{F}↾}_{{C}}\right)}^{-1}={C}$
16 14 15 syl ${⊢}{\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{1-1 onto}{⟶}{C}\to \mathrm{ran}{\left({{F}↾}_{{C}}\right)}^{-1}={C}$
17 11 13 16 3eqtr3a ${⊢}{\left({{F}↾}_{{C}}\right)}^{-1}:{F}\left[{C}\right]\underset{1-1 onto}{⟶}{C}\to {\left({{F}↾}_{{C}}\right)}^{-1}\left[{F}\left[{C}\right]\right]={C}$
18 10 17 syl ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to {\left({{F}↾}_{{C}}\right)}^{-1}\left[{F}\left[{C}\right]\right]={C}$
19 7 18 eqtr3d ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to \left({{{F}}^{-1}↾}_{{F}\left[{C}\right]}\right)\left[{F}\left[{C}\right]\right]={C}$
20 1 19 syl5eqr ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {C}\subseteq {A}\right)\to {{F}}^{-1}\left[{F}\left[{C}\right]\right]={C}$