# Metamath Proof Explorer

## Theorem f1ocnvfv3

Description: Value of the converse of a one-to-one onto function. (Contributed by NM, 26-May-2006) (Proof shortened by Mario Carneiro, 24-Dec-2016)

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

### Proof

Step Hyp Ref Expression
1 f1ocnvdm ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to {{F}}^{-1}\left({C}\right)\in {A}$
2 f1ocnvfvb ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {x}\in {A}\wedge {C}\in {B}\right)\to \left({F}\left({x}\right)={C}↔{{F}}^{-1}\left({C}\right)={x}\right)$
3 2 3expa ${⊢}\left(\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {x}\in {A}\right)\wedge {C}\in {B}\right)\to \left({F}\left({x}\right)={C}↔{{F}}^{-1}\left({C}\right)={x}\right)$
4 3 an32s ${⊢}\left(\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={C}↔{{F}}^{-1}\left({C}\right)={x}\right)$
5 eqcom ${⊢}{x}={{F}}^{-1}\left({C}\right)↔{{F}}^{-1}\left({C}\right)={x}$
6 4 5 syl6bbr ${⊢}\left(\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={C}↔{x}={{F}}^{-1}\left({C}\right)\right)$
7 1 6 riota5 ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \left(\iota {x}\in {A}|{F}\left({x}\right)={C}\right)={{F}}^{-1}\left({C}\right)$
8 7 eqcomd ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to {{F}}^{-1}\left({C}\right)=\left(\iota {x}\in {A}|{F}\left({x}\right)={C}\right)$