# Metamath Proof Explorer

## Theorem f1ofveu

Description: There is one domain element for each value of a one-to-one onto function. (Contributed by NM, 26-May-2006)

Ref Expression
Assertion f1ofveu ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={C}$

### Proof

Step Hyp Ref Expression
1 f1ocnv ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}$
2 f1of ${⊢}{{F}}^{-1}:{B}\underset{1-1 onto}{⟶}{A}\to {{F}}^{-1}:{B}⟶{A}$
3 1 2 syl ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}:{B}⟶{A}$
4 feu ${⊢}\left({{F}}^{-1}:{B}⟶{A}\wedge {C}\in {B}\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}⟨{C},{x}⟩\in {{F}}^{-1}$
5 3 4 sylan ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}⟨{C},{x}⟩\in {{F}}^{-1}$
6 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)$
7 6 3com23 ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={C}↔{{F}}^{-1}\left({C}\right)={x}\right)$
8 dff1o4 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}Fn{A}\wedge {{F}}^{-1}Fn{B}\right)$
9 8 simprbi ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}\to {{F}}^{-1}Fn{B}$
10 fnopfvb ${⊢}\left({{F}}^{-1}Fn{B}\wedge {C}\in {B}\right)\to \left({{F}}^{-1}\left({C}\right)={x}↔⟨{C},{x}⟩\in {{F}}^{-1}\right)$
11 10 3adant3 ${⊢}\left({{F}}^{-1}Fn{B}\wedge {C}\in {B}\wedge {x}\in {A}\right)\to \left({{F}}^{-1}\left({C}\right)={x}↔⟨{C},{x}⟩\in {{F}}^{-1}\right)$
12 9 11 syl3an1 ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\wedge {x}\in {A}\right)\to \left({{F}}^{-1}\left({C}\right)={x}↔⟨{C},{x}⟩\in {{F}}^{-1}\right)$
13 7 12 bitrd ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\wedge {x}\in {A}\right)\to \left({F}\left({x}\right)={C}↔⟨{C},{x}⟩\in {{F}}^{-1}\right)$
14 13 3expa ${⊢}\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}↔⟨{C},{x}⟩\in {{F}}^{-1}\right)$
15 14 reubidva ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \left(\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={C}↔\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}⟨{C},{x}⟩\in {{F}}^{-1}\right)$
16 5 15 mpbird ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{B}\wedge {C}\in {B}\right)\to \exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={C}$