# Metamath Proof Explorer

## Theorem dff1o5

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

Ref Expression
Assertion dff1o5 ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}={B}\right)$

### Proof

Step Hyp Ref Expression
1 df-f1o ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)$
2 f1f ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to {F}:{A}⟶{B}$
3 2 biantrurd ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to \left(\mathrm{ran}{F}={B}↔\left({F}:{A}⟶{B}\wedge \mathrm{ran}{F}={B}\right)\right)$
4 dffo2 ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{ran}{F}={B}\right)$
5 3 4 syl6rbbr ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to \left({F}:{A}\underset{onto}{⟶}{B}↔\mathrm{ran}{F}={B}\right)$
6 5 pm5.32i ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge {F}:{A}\underset{onto}{⟶}{B}\right)↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}={B}\right)$
7 1 6 bitri ${⊢}{F}:{A}\underset{1-1 onto}{⟶}{B}↔\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}={B}\right)$