# Metamath Proof Explorer

## Theorem dffo3f

Description: An onto mapping expressed in terms of function values. As dffo3 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis dffo3f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
Assertion dffo3f ${⊢}{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 dffo3f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 dffo2 ${⊢}{F}:{A}\underset{onto}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{ran}{F}={B}\right)$
3 ffn ${⊢}{F}:{A}⟶{B}\to {F}Fn{A}$
4 fnrnfv ${⊢}{F}Fn{A}\to \mathrm{ran}{F}=\left\{{y}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({w}\right)\right\}$
5 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{w}$
6 1 5 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)$
7 6 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={F}\left({w}\right)$
8 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)$
9 fveq2 ${⊢}{w}={x}\to {F}\left({w}\right)={F}\left({x}\right)$
10 9 eqeq2d ${⊢}{w}={x}\to \left({y}={F}\left({w}\right)↔{y}={F}\left({x}\right)\right)$
11 7 8 10 cbvrexw ${⊢}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({w}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)$
12 11 abbii ${⊢}\left\{{y}|\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({w}\right)\right\}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$
13 4 12 syl6eq ${⊢}{F}Fn{A}\to \mathrm{ran}{F}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$
14 13 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)$
15 3 14 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)$
16 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
17 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
18 1 16 17 nff ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}:{A}⟶{B}$
19 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
20 simpr ${⊢}\left(\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\wedge {y}={F}\left({x}\right)\right)\to {y}={F}\left({x}\right)$
21 ffvelrn ${⊢}\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in {B}$
22 21 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}$
23 20 22 eqeltrd ${⊢}\left(\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\wedge {y}={F}\left({x}\right)\right)\to {y}\in {B}$
24 18 19 23 rexlimd3 ${⊢}{F}:{A}⟶{B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\to {y}\in {B}\right)$
25 24 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)$
26 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)$
27 25 26 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)$
28 27 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)$
29 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)$
30 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)$
31 28 29 30 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)$
32 15 31 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)$
33 32 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)$
34 2 33 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)$