ffoss

Description: Relationship between a mapping and an onto mapping. Figure 38 of Enderton p. 145. (Contributed by NM, 10-May-1998)

		Ref	Expression
	Hypothesis	f11o.1	$⊢ F \in V$
	Assertion	ffoss	$⊢ F : A ⟶ B \leftrightarrow \exists x (F : A \underset{onto}{⟶} x \land x \subseteq B)$

Step	Hyp	Ref	Expression
1		f11o.1	$⊢ F \in V$
2		df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$
3		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
4	3	anbi1i	$⊢ (F Fn A \land ran F \subseteq B) \leftrightarrow (F : A \underset{onto}{⟶} ran F \land ran F \subseteq B)$
5	2 4	bitri	$⊢ F : A ⟶ B \leftrightarrow (F : A \underset{onto}{⟶} ran F \land ran F \subseteq B)$
6	1	rnex	$⊢ ran F \in V$
7		foeq3	$⊢ x = ran F \to (F : A \underset{onto}{⟶} x \leftrightarrow F : A \underset{onto}{⟶} ran F)$
8		sseq1	$⊢ x = ran F \to (x \subseteq B \leftrightarrow ran F \subseteq B)$
9	7 8	anbi12d	$⊢ x = ran F \to ((F : A \underset{onto}{⟶} x \land x \subseteq B) \leftrightarrow (F : A \underset{onto}{⟶} ran F \land ran F \subseteq B))$
10	6 9	spcev	$⊢ (F : A \underset{onto}{⟶} ran F \land ran F \subseteq B) \to \exists x (F : A \underset{onto}{⟶} x \land x \subseteq B)$
11	5 10	sylbi	$⊢ F : A ⟶ B \to \exists x (F : A \underset{onto}{⟶} x \land x \subseteq B)$
12		fof	$⊢ F : A \underset{onto}{⟶} x \to F : A ⟶ x$
13		fss	$⊢ (F : A ⟶ x \land x \subseteq B) \to F : A ⟶ B$
14	12 13	sylan	$⊢ (F : A \underset{onto}{⟶} x \land x \subseteq B) \to F : A ⟶ B$
15	14	exlimiv	$⊢ \exists x (F : A \underset{onto}{⟶} x \land x \subseteq B) \to F : A ⟶ B$
16	11 15	impbii	$⊢ F : A ⟶ B \leftrightarrow \exists x (F : A \underset{onto}{⟶} x \land x \subseteq B)$

Metamath Proof Explorer