dffo5

Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007)

		Ref	Expression
	Assertion	dffo5	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists x x F y)$

Step	Hyp	Ref	Expression
1		dffo4	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists x \in A x F y)$
2		rexex	$⊢ \exists x \in A x F y \to \exists x x F y$
3	2	ralimi	$⊢ \forall y \in B \exists x \in A x F y \to \forall y \in B \exists x x F y$
4	3	anim2i	$⊢ (F : A ⟶ B \land \forall y \in B \exists x \in A x F y) \to (F : A ⟶ B \land \forall y \in B \exists x x F y)$
5		ffn	$⊢ F : A ⟶ B \to F Fn A$
6		fnbr	$⊢ (F Fn A \land x F y) \to x \in A$
7	6	ex	$⊢ F Fn A \to (x F y \to x \in A)$
8	5 7	syl	$⊢ F : A ⟶ B \to (x F y \to x \in A)$
9	8	ancrd	$⊢ F : A ⟶ B \to (x F y \to (x \in A \land x F y))$
10	9	eximdv	$⊢ F : A ⟶ B \to (\exists x x F y \to \exists x (x \in A \land x F y))$
11		df-rex	$⊢ \exists x \in A x F y \leftrightarrow \exists x (x \in A \land x F y)$
12	10 11	imbitrrdi	$⊢ F : A ⟶ B \to (\exists x x F y \to \exists x \in A x F y)$
13	12	ralimdv	$⊢ F : A ⟶ B \to (\forall y \in B \exists x x F y \to \forall y \in B \exists x \in A x F y)$
14	13	imdistani	$⊢ (F : A ⟶ B \land \forall y \in B \exists x x F y) \to (F : A ⟶ B \land \forall y \in B \exists x \in A x F y)$
15	4 14	impbii	$⊢ (F : A ⟶ B \land \forall y \in B \exists x \in A x F y) \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists x x F y)$
16	1 15	bitri	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists x x F y)$

Metamath Proof Explorer