# Metamath Proof Explorer

## Theorem f1ocnvfv2

Description: The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004)

Ref Expression
Assertion f1ocnvfv2 ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to {F}\left({{F}}^{-1}\left({C}\right)\right)={C}$

### Proof

Step Hyp Ref Expression
1 f1ococnv2 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {F}\circ {{F}}^{-1}={\mathrm{I}↾}_{{B}}$
2 1 fveq1d ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to \left({F}\circ {{F}}^{-1}\right)\left({C}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({C}\right)$
3 2 adantr ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \left({F}\circ {{F}}^{-1}\right)\left({C}\right)=\left({\mathrm{I}↾}_{{B}}\right)\left({C}\right)$
4 f1ocnv ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$
5 f1of ${⊢}{{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{F}}^{-1}:{B}⟶{A}$
6 4 5 syl ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}⟶{A}$
7 fvco3 ${⊢}\left({{F}}^{-1}:{B}⟶{A}\wedge {C}\in {B}\right)\to \left({F}\circ {{F}}^{-1}\right)\left({C}\right)={F}\left({{F}}^{-1}\left({C}\right)\right)$
8 6 7 sylan ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \left({F}\circ {{F}}^{-1}\right)\left({C}\right)={F}\left({{F}}^{-1}\left({C}\right)\right)$
9 fvresi ${⊢}{C}\in {B}\to \left({\mathrm{I}↾}_{{B}}\right)\left({C}\right)={C}$
10 9 adantl ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \left({\mathrm{I}↾}_{{B}}\right)\left({C}\right)={C}$
11 3 8 10 3eqtr3d ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to {F}\left({{F}}^{-1}\left({C}\right)\right)={C}$