# Metamath Proof Explorer

## Theorem nffo

Description: Bound-variable hypothesis builder for an onto function. (Contributed by NM, 16-May-2004)

Ref Expression
Hypotheses nffo.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
nffo.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nffo.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nffo ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}:{A}\underset{onto}{⟶}{B}$

### Proof

Step Hyp Ref Expression
1 nffo.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 nffo.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nffo.3 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
4 df-fo ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)$
5 1 2 nffn ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}Fn{A}$
6 1 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}$
7 6 3 nfeq ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}{F}={B}$
8 5 7 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({F}Fn{A}\wedge \mathrm{ran}{F}={B}\right)$
9 4 8 nfxfr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}:{A}\underset{onto}{⟶}{B}$