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{\_}{Ⅎ}xF$$
Assertion	dffo3f	$$⊢F:A\underset{onto}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall y\in B\exists x\in Ay=F\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffo3f.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		dffo2	$$⊢F:A\underset{onto}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \mathrm{ran}F=B\right)$$
3		ffn	$$⊢F:A⟶B\to FFnA$$
4		fnrnfv	$$⊢FFnA\to \mathrm{ran}F=\left\{y|\exists w\in Ay=F\left(w\right)\right\}$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
6	1 5	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(w\right)$$
7	6	nfeq2	$$⊢Ⅎxy=F\left(w\right)$$
8		nfv	$$⊢Ⅎwy=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)\leftrightarrow y=F\left(x\right)\right)$$
11	7 8 10	cbvrexw	$$⊢\exists w\in Ay=F\left(w\right)\leftrightarrow \exists x\in Ay=F\left(x\right)$$
12	11	abbii	$$⊢\left\{y|\exists w\in Ay=F\left(w\right)\right\}=\left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
13	4 12	eqtrdi	$$⊢FFnA\to \mathrm{ran}F=\left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
14	13	eqeq1d	$$⊢FFnA\to \left(\mathrm{ran}F=B\leftrightarrow \left\{y|\exists x\in Ay=F\left(x\right)\right\}=B\right)$$
15	3 14	syl	$$⊢F:A⟶B\to \left(\mathrm{ran}F=B\leftrightarrow \left\{y|\exists x\in Ay=F\left(x\right)\right\}=B\right)$$
16		dfbi2	$$⊢\left(\exists x\in Ay=F\left(x\right)\leftrightarrow y\in B\right)\leftrightarrow \left(\left(\exists x\in Ay=F\left(x\right)\to y\in B\right)\wedge \left(y\in B\to \exists x\in Ay=F\left(x\right)\right)\right)$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
19	1 17 18	nff	$$⊢ℲxF:A⟶B$$
20		nfv	$$⊢Ⅎxy\in B$$
21		simpr	$$⊢\left(\left(F:A⟶B\wedge x\in A\right)\wedge y=F\left(x\right)\right)\to y=F\left(x\right)$$
22		ffvelrn	$$⊢\left(F:A⟶B\wedge x\in A\right)\to F\left(x\right)\in B$$
23	22	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$$
24	21 23	eqeltrd	$$⊢\left(\left(F:A⟶B\wedge x\in A\right)\wedge y=F\left(x\right)\right)\to y\in B$$
25	19 20 24	rexlimd3	$$⊢F:A⟶B\to \left(\exists x\in Ay=F\left(x\right)\to y\in B\right)$$
26	25	biantrurd	$$⊢F:A⟶B\to \left(\left(y\in B\to \exists x\in Ay=F\left(x\right)\right)\leftrightarrow \left(\left(\exists x\in Ay=F\left(x\right)\to y\in B\right)\wedge \left(y\in B\to \exists x\in Ay=F\left(x\right)\right)\right)\right)$$
27	16 26	bitr4id	$$⊢F:A⟶B\to \left(\left(\exists x\in Ay=F\left(x\right)\leftrightarrow y\in B\right)\leftrightarrow \left(y\in B\to \exists x\in Ay=F\left(x\right)\right)\right)$$
28	27	albidv	$$⊢F:A⟶B\to \left(\forall y\left(\exists x\in Ay=F\left(x\right)\leftrightarrow y\in B\right)\leftrightarrow \forall y\left(y\in B\to \exists x\in Ay=F\left(x\right)\right)\right)$$
29		abeq1	$$⊢\left\{y|\exists x\in Ay=F\left(x\right)\right\}=B\leftrightarrow \forall y\left(\exists x\in Ay=F\left(x\right)\leftrightarrow y\in B\right)$$
30		df-ral	$$⊢\forall y\in B\exists x\in Ay=F\left(x\right)\leftrightarrow \forall y\left(y\in B\to \exists x\in Ay=F\left(x\right)\right)$$
31	28 29 30	3bitr4g	$$⊢F:A⟶B\to \left(\left\{y|\exists x\in Ay=F\left(x\right)\right\}=B\leftrightarrow \forall y\in B\exists x\in Ay=F\left(x\right)\right)$$
32	15 31	bitrd	$$⊢F:A⟶B\to \left(\mathrm{ran}F=B\leftrightarrow \forall y\in B\exists x\in Ay=F\left(x\right)\right)$$
33	32	pm5.32i	$$⊢\left(F:A⟶B\wedge \mathrm{ran}F=B\right)\leftrightarrow \left(F:A⟶B\wedge \forall y\in B\exists x\in Ay=F\left(x\right)\right)$$
34	2 33	bitri	$$⊢F:A\underset{onto}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall y\in B\exists x\in Ay=F\left(x\right)\right)$$