fconst3

Description: Two ways to express a constant function. (Contributed by NM, 15-Mar-2007)

		Ref	Expression
	Assertion	fconst3	$⊢ F : A ⟶ \{B\} \leftrightarrow (F Fn A \land A \subseteq F^{-1} [\{B\}])$

Step	Hyp	Ref	Expression
1		fconstfv	$⊢ F : A ⟶ \{B\} \leftrightarrow (F Fn A \land \forall x \in A F (x) = B)$
2		fnfun	$⊢ F Fn A \to Fun F$
3		fndm	$⊢ F Fn A \to dom F = A$
4		eqimss2	$⊢ dom F = A \to A \subseteq dom F$
5	3 4	syl	$⊢ F Fn A \to A \subseteq dom F$
6		funconstss	$⊢ (Fun F \land A \subseteq dom F) \to (\forall x \in A F (x) = B \leftrightarrow A \subseteq F^{-1} [\{B\}])$
7	2 5 6	syl2anc	$⊢ F Fn A \to (\forall x \in A F (x) = B \leftrightarrow A \subseteq F^{-1} [\{B\}])$
8	7	pm5.32i	$⊢ (F Fn A \land \forall x \in A F (x) = B) \leftrightarrow (F Fn A \land A \subseteq F^{-1} [\{B\}])$
9	1 8	bitri	$⊢ F : A ⟶ \{B\} \leftrightarrow (F Fn A \land A \subseteq F^{-1} [\{B\}])$

Metamath Proof Explorer