# Metamath Proof Explorer

## Theorem f1ocnvfvb

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

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

### Proof

Step Hyp Ref Expression
1 f1ocnvfv ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {A}\right)\to \left({F}\left({C}\right)={D}\to {{F}}^{-1}\left({D}\right)={C}\right)$
2 1 3adant3 ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {A}\wedge {D}\in {B}\right)\to \left({F}\left({C}\right)={D}\to {{F}}^{-1}\left({D}\right)={C}\right)$
3 fveq2 ${⊢}{C}={{F}}^{-1}\left({D}\right)\to {F}\left({C}\right)={F}\left({{F}}^{-1}\left({D}\right)\right)$
4 3 eqcoms ${⊢}{{F}}^{-1}\left({D}\right)={C}\to {F}\left({C}\right)={F}\left({{F}}^{-1}\left({D}\right)\right)$
5 f1ocnvfv2 ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {D}\in {B}\right)\to {F}\left({{F}}^{-1}\left({D}\right)\right)={D}$
6 5 eqeq2d ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {D}\in {B}\right)\to \left({F}\left({C}\right)={F}\left({{F}}^{-1}\left({D}\right)\right)↔{F}\left({C}\right)={D}\right)$
7 4 6 syl5ib ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {D}\in {B}\right)\to \left({{F}}^{-1}\left({D}\right)={C}\to {F}\left({C}\right)={D}\right)$
8 7 3adant2 ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {A}\wedge {D}\in {B}\right)\to \left({{F}}^{-1}\left({D}\right)={C}\to {F}\left({C}\right)={D}\right)$
9 2 8 impbid ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {A}\wedge {D}\in {B}\right)\to \left({F}\left({C}\right)={D}↔{{F}}^{-1}\left({D}\right)={C}\right)$