dffo4

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

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

Proof

Step	Hyp	Ref	Expression
1		dffo2	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land ran F = B)$
2		simpl	$⊢ (F : A ⟶ B \land ran F = B) \to F : A ⟶ B$
3		vex	$⊢ y \in V$
4	3	elrn	$⊢ y \in ran F \leftrightarrow \exists x x F y$
5		eleq2	$⊢ ran F = B \to (y \in ran F \leftrightarrow y \in B)$
6	4 5	bitr3id	$⊢ ran F = B \to (\exists x x F y \leftrightarrow y \in B)$
7	6	biimpar	$⊢ (ran F = B \land y \in B) \to \exists x x F y$
8	7	adantll	$⊢ ((F : A ⟶ B \land ran F = B) \land y \in B) \to \exists x x F y$
9		ffn	$⊢ F : A ⟶ B \to F Fn A$
10		fnbr	$⊢ (F Fn A \land x F y) \to x \in A$
11	10	ex	$⊢ F Fn A \to (x F y \to x \in A)$
12	9 11	syl	$⊢ F : A ⟶ B \to (x F y \to x \in A)$
13	12	ancrd	$⊢ F : A ⟶ B \to (x F y \to (x \in A \land x F y))$
14	13	eximdv	$⊢ F : A ⟶ B \to (\exists x x F y \to \exists x (x \in A \land x F y))$
15		df-rex	$⊢ \exists x \in A x F y \leftrightarrow \exists x (x \in A \land x F y)$
16	14 15	imbitrrdi	$⊢ F : A ⟶ B \to (\exists x x F y \to \exists x \in A x F y)$
17	16	ad2antrr	$⊢ ((F : A ⟶ B \land ran F = B) \land y \in B) \to (\exists x x F y \to \exists x \in A x F y)$
18	8 17	mpd	$⊢ ((F : A ⟶ B \land ran F = B) \land y \in B) \to \exists x \in A x F y$
19	18	ralrimiva	$⊢ (F : A ⟶ B \land ran F = B) \to \forall y \in B \exists x \in A x F y$
20	2 19	jca	$⊢ (F : A ⟶ B \land ran F = B) \to (F : A ⟶ B \land \forall y \in B \exists x \in A x F y)$
21	1 20	sylbi	$⊢ F : A \underset{onto}{⟶} B \to (F : A ⟶ B \land \forall y \in B \exists x \in A x F y)$
22		fnbrfvb	$⊢ (F Fn A \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
23	22	biimprd	$⊢ (F Fn A \land x \in A) \to (x F y \to F (x) = y)$
24		eqcom	$⊢ F (x) = y \leftrightarrow y = F (x)$
25	23 24	imbitrdi	$⊢ (F Fn A \land x \in A) \to (x F y \to y = F (x))$
26	9 25	sylan	$⊢ (F : A ⟶ B \land x \in A) \to (x F y \to y = F (x))$
27	26	reximdva	$⊢ F : A ⟶ B \to (\exists x \in A x F y \to \exists x \in A y = F (x))$
28	27	ralimdv	$⊢ F : A ⟶ B \to (\forall y \in B \exists x \in A x F y \to \forall y \in B \exists x \in A y = F (x))$
29	28	imdistani	$⊢ (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 \in A y = F (x))$
30		dffo3	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists x \in A y = F (x))$
31	29 30	sylibr	$⊢ (F : A ⟶ B \land \forall y \in B \exists x \in A x F y) \to F : A \underset{onto}{⟶} B$
32	21 31	impbii	$⊢ F : A \underset{onto}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall y \in B \exists x \in A x F y)$

Metamath Proof Explorer

Theorem dffo4

Proof