funssxp

Description: Two ways of specifying a partial function from A to B . (Contributed by NM, 13-Nov-2007)

		Ref	Expression
	Assertion	funssxp	$⊢ (Fun F \land F \subseteq A \times B) \leftrightarrow (F : dom F ⟶ B \land dom F \subseteq A)$

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2	1	biimpi	$⊢ Fun F \to F Fn dom F$
3		rnss	$⊢ F \subseteq A \times B \to ran F \subseteq ran (A \times B)$
4		rnxpss	$⊢ ran (A \times B) \subseteq B$
5	3 4	sstrdi	$⊢ F \subseteq A \times B \to ran F \subseteq B$
6	2 5	anim12i	$⊢ (Fun F \land F \subseteq A \times B) \to (F Fn dom F \land ran F \subseteq B)$
7		df-f	$⊢ F : dom F ⟶ B \leftrightarrow (F Fn dom F \land ran F \subseteq B)$
8	6 7	sylibr	$⊢ (Fun F \land F \subseteq A \times B) \to F : dom F ⟶ B$
9		dmss	$⊢ F \subseteq A \times B \to dom F \subseteq dom (A \times B)$
10		dmxpss	$⊢ dom (A \times B) \subseteq A$
11	9 10	sstrdi	$⊢ F \subseteq A \times B \to dom F \subseteq A$
12	11	adantl	$⊢ (Fun F \land F \subseteq A \times B) \to dom F \subseteq A$
13	8 12	jca	$⊢ (Fun F \land F \subseteq A \times B) \to (F : dom F ⟶ B \land dom F \subseteq A)$
14		ffun	$⊢ F : dom F ⟶ B \to Fun F$
15	14	adantr	$⊢ (F : dom F ⟶ B \land dom F \subseteq A) \to Fun F$
16		fssxp	$⊢ F : dom F ⟶ B \to F \subseteq dom F \times B$
17		xpss1	$⊢ dom F \subseteq A \to dom F \times B \subseteq A \times B$
18	16 17	sylan9ss	$⊢ (F : dom F ⟶ B \land dom F \subseteq A) \to F \subseteq A \times B$
19	15 18	jca	$⊢ (F : dom F ⟶ B \land dom F \subseteq A) \to (Fun F \land F \subseteq A \times B)$
20	13 19	impbii	$⊢ (Fun F \land F \subseteq A \times B) \leftrightarrow (F : dom F ⟶ B \land dom F \subseteq A)$

Metamath Proof Explorer