constcof

Description: Composition with a constant function. See also fcoconst . (Contributed by Thierry Arnoux, 11-Jan-2026)

Step	Hyp	Ref	Expression
1		constcof.1	$⊢ φ \to F : X ⟶ I$
2		constcof.2	$⊢ φ \to Y \in V$
3		fnconstg	$⊢ Y \in V \to (I \times \{Y\}) Fn I$
4	2 3	syl	$⊢ φ \to (I \times \{Y\}) Fn I$
5		fnfco	$⊢ ((I \times \{Y\}) Fn I \land F : X ⟶ I) \to ((I \times \{Y\}) \circ F) Fn X$
6	4 1 5	syl2anc	$⊢ φ \to ((I \times \{Y\}) \circ F) Fn X$
7	1	adantr	$⊢ (φ \land x \in X) \to F : X ⟶ I$
8		simpr	$⊢ (φ \land x \in X) \to x \in X$
9	7 8	fvco3d	$⊢ (φ \land x \in X) \to ((I \times \{Y\}) \circ F) (x) = (I \times \{Y\}) (F (x))$
10	2	adantr	$⊢ (φ \land x \in X) \to Y \in V$
11	1	ffvelcdmda	$⊢ (φ \land x \in X) \to F (x) \in I$
12		fvconst2g	$⊢ (Y \in V \land F (x) \in I) \to (I \times \{Y\}) (F (x)) = Y$
13	10 11 12	syl2anc	$⊢ (φ \land x \in X) \to (I \times \{Y\}) (F (x)) = Y$
14	9 13	eqtrd	$⊢ (φ \land x \in X) \to ((I \times \{Y\}) \circ F) (x) = Y$
15	6 14	fconst7v	$⊢ φ \to (I \times \{Y\}) \circ F = X \times \{Y\}$

Metamath Proof Explorer