Theorem foov

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

	Ref	Expression
Assertion	foov	$$⊢F:A\times B\underset{onto}{⟶}C\leftrightarrow \left(F:A\times B⟶C\wedge \forall z\in C\exists x\in A\exists y\in Bz=xFy\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffo3	$$⊢F:A\times B\underset{onto}{⟶}C\leftrightarrow \left(F:A\times B⟶C\wedge \forall z\in C\exists w\in \left(A\times B\right)z=F\left(w\right)\right)$$
2		fveq2	$$⊢w=⟨x,y⟩\to F\left(w\right)=F\left(⟨x,y⟩\right)$$
3		df-ov	$$⊢xFy=F\left(⟨x,y⟩\right)$$
4	2 3	eqtr4di	$$⊢w=⟨x,y⟩\to F\left(w\right)=xFy$$
5	4	eqeq2d	$$⊢w=⟨x,y⟩\to \left(z=F\left(w\right)\leftrightarrow z=xFy\right)$$
6	5	rexxp	$$⊢\exists w\in \left(A\times B\right)z=F\left(w\right)\leftrightarrow \exists x\in A\exists y\in Bz=xFy$$
7	6	ralbii	$$⊢\forall z\in C\exists w\in \left(A\times B\right)z=F\left(w\right)\leftrightarrow \forall z\in C\exists x\in A\exists y\in Bz=xFy$$
8	7	anbi2i	$$⊢\left(F:A\times B⟶C\wedge \forall z\in C\exists w\in \left(A\times B\right)z=F\left(w\right)\right)\leftrightarrow \left(F:A\times B⟶C\wedge \forall z\in C\exists x\in A\exists y\in Bz=xFy\right)$$
9	1 8	bitri	$$⊢F:A\times B\underset{onto}{⟶}C\leftrightarrow \left(F:A\times B⟶C\wedge \forall z\in C\exists x\in A\exists y\in Bz=xFy\right)$$