fdmrn

Description: A different way to write F is a function. (Contributed by Thierry Arnoux, 7-Dec-2016)

		Ref	Expression
	Assertion	fdmrn	$⊢ Fun F \leftrightarrow F : dom F ⟶ ran F$

Step	Hyp	Ref	Expression
1		ssid	$⊢ ran F \subseteq ran F$
2		df-f	$⊢ F : dom F ⟶ ran F \leftrightarrow (F Fn dom F \land ran F \subseteq ran F)$
3	1 2	mpbiran2	$⊢ F : dom F ⟶ ran F \leftrightarrow F Fn dom F$
4		eqid	$⊢ dom F = dom F$
5		df-fn	$⊢ F Fn dom F \leftrightarrow (Fun F \land dom F = dom F)$
6	4 5	mpbiran2	$⊢ F Fn dom F \leftrightarrow Fun F$
7	3 6	bitr2i	$⊢ Fun F \leftrightarrow F : dom F ⟶ ran F$

Metamath Proof Explorer