# Metamath Proof Explorer

## Theorem f11o

Description: Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998)

Ref Expression
Hypothesis f11o.1 ${⊢}{F}\in \mathrm{V}$
Assertion f11o ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{1-1 onto}{⟶}{x}\wedge {x}\subseteq {B}\right)$

### Proof

Step Hyp Ref Expression
1 f11o.1 ${⊢}{F}\in \mathrm{V}$
2 1 ffoss ${⊢}{F}:{A}⟶{B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)$
3 2 anbi1i ${⊢}\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)$
4 df-f1 ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
5 dff1o3 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{x}↔\left({F}:{A}\underset{onto}{⟶}{x}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
6 5 anbi1i ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{x}\wedge {x}\subseteq {B}\right)↔\left(\left({F}:{A}\underset{onto}{⟶}{x}\wedge \mathrm{Fun}{{F}}^{-1}\right)\wedge {x}\subseteq {B}\right)$
7 an32 ${⊢}\left(\left({F}:{A}\underset{onto}{⟶}{x}\wedge \mathrm{Fun}{{F}}^{-1}\right)\wedge {x}\subseteq {B}\right)↔\left(\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)$
8 6 7 bitri ${⊢}\left({F}:{A}\underset{1-1 onto}{⟶}{x}\wedge {x}\subseteq {B}\right)↔\left(\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)$
9 8 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{1-1 onto}{⟶}{x}\wedge {x}\subseteq {B}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)$
10 19.41v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)$
11 9 10 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{1-1 onto}{⟶}{x}\wedge {x}\subseteq {B}\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{onto}{⟶}{x}\wedge {x}\subseteq {B}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)$
12 3 4 11 3bitr4i ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({F}:{A}\underset{1-1 onto}{⟶}{x}\wedge {x}\subseteq {B}\right)$