Theorem nffo

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

	Ref	Expression
Hypotheses	nffo.1	$$⊢\underset{\_}{Ⅎ}xF$$
	nffo.2	$$⊢\underset{\_}{Ⅎ}xA$$
	nffo.3	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nffo	$$⊢ℲxF:A\underset{onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		nffo.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nffo.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nffo.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		df-fo	$$⊢F:A\underset{onto}{⟶}B\leftrightarrow \left(FFnA\wedge \mathrm{ran}F=B\right)$$
5	1 2	nffn	$$⊢ℲxFFnA$$
6	1	nfrn	$$⊢\underset{\_}{Ⅎ}x\mathrm{ran}F$$
7	6 3	nfeq	$$⊢Ⅎx\mathrm{ran}F=B$$
8	5 7	nfan	$$⊢Ⅎx\left(FFnA\wedge \mathrm{ran}F=B\right)$$
9	4 8	nfxfr	$$⊢ℲxF:A\underset{onto}{⟶}B$$