# Metamath Proof Explorer

## Theorem dffo3

Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006)

Ref Expression
Assertion dffo3 ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 dffo2 ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{ran}{F}={B}\right)$
2 ffn ${⊢}{F}:{A}⟶{B}\to {F}Fn{A}$
3 fnrnfv ${⊢}{F}Fn{A}\to \mathrm{ran}{F}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$
4 3 eqeq1d ${⊢}{F}Fn{A}\to \left(\mathrm{ran}{F}={B}↔\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}={B}\right)$
5 2 4 syl ${⊢}{F}:{A}⟶{B}\to \left(\mathrm{ran}{F}={B}↔\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}={B}\right)$
6 simpr ${⊢}\left(\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\wedge {y}={F}\left({x}\right)\right)\to {y}={F}\left({x}\right)$
7 ffvelrn ${⊢}\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in {B}$
8 7 adantr ${⊢}\left(\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\wedge {y}={F}\left({x}\right)\right)\to {F}\left({x}\right)\in {B}$
9 6 8 eqeltrd ${⊢}\left(\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\wedge {y}={F}\left({x}\right)\right)\to {y}\in {B}$
10 9 rexlimdva2 ${⊢}{F}:{A}⟶{B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\to {y}\in {B}\right)$
11 10 biantrurd ${⊢}{F}:{A}⟶{B}\to \left(\left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)↔\left(\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\to {y}\in {B}\right)\wedge \left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)\right)\right)$
12 dfbi2 ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)↔{y}\in {B}\right)↔\left(\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\to {y}\in {B}\right)\wedge \left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)\right)$
13 11 12 syl6rbbr ${⊢}{F}:{A}⟶{B}\to \left(\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)↔{y}\in {B}\right)↔\left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)\right)$
14 13 albidv ${⊢}{F}:{A}⟶{B}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)↔{y}\in {B}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)\right)$
15 abeq1 ${⊢}\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}={B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)↔{y}\in {B}\right)$
16 df-ral ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)$
17 14 15 16 3bitr4g ${⊢}{F}:{A}⟶{B}\to \left(\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}={B}↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)$
18 5 17 bitrd ${⊢}{F}:{A}⟶{B}\to \left(\mathrm{ran}{F}={B}↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)$
19 18 pm5.32i ${⊢}\left({F}:{A}⟶{B}\wedge \mathrm{ran}{F}={B}\right)↔\left({F}:{A}⟶{B}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)$
20 1 19 bitri ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right)$