# Metamath Proof Explorer

## Theorem dff1o4

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion dff1o4 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}Fn{A}\wedge {{F}}^{-1}Fn{B}\right)$

### Proof

Step Hyp Ref Expression
1 dff1o2 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}Fn{A}\wedge \mathrm{Fun}{{F}}^{-1}\wedge \mathrm{ran}{F}={B}\right)$
2 3anass ${⊢}\left({F}Fn{A}\wedge \mathrm{Fun}{{F}}^{-1}\wedge \mathrm{ran}{F}={B}\right)↔\left({F}Fn{A}\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge \mathrm{ran}{F}={B}\right)\right)$
3 df-rn ${⊢}\mathrm{ran}{F}=\mathrm{dom}{{F}}^{-1}$
4 3 eqeq1i ${⊢}\mathrm{ran}{F}={B}↔\mathrm{dom}{{F}}^{-1}={B}$
5 4 anbi2i ${⊢}\left(\mathrm{Fun}{{F}}^{-1}\wedge \mathrm{ran}{F}={B}\right)↔\left(\mathrm{Fun}{{F}}^{-1}\wedge \mathrm{dom}{{F}}^{-1}={B}\right)$
6 df-fn ${⊢}{{F}}^{-1}Fn{B}↔\left(\mathrm{Fun}{{F}}^{-1}\wedge \mathrm{dom}{{F}}^{-1}={B}\right)$
7 5 6 bitr4i ${⊢}\left(\mathrm{Fun}{{F}}^{-1}\wedge \mathrm{ran}{F}={B}\right)↔{{F}}^{-1}Fn{B}$
8 7 anbi2i ${⊢}\left({F}Fn{A}\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge \mathrm{ran}{F}={B}\right)\right)↔\left({F}Fn{A}\wedge {{F}}^{-1}Fn{B}\right)$
9 1 2 8 3bitri ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}Fn{A}\wedge {{F}}^{-1}Fn{B}\right)$