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 (F : A \times B ⟶ C \land \forall z \in C \exists x \in A \exists y \in B z = x F y)$

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

Metamath Proof Explorer