ofcf

Description: The function/constant operation produces a function. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Hypotheses	ofcf.1	$⊢ (φ \land (x \in S \land y \in T)) \to x R y \in U$
	ofcf.2	$⊢ φ \to F : A ⟶ S$
	ofcf.4	$⊢ φ \to A \in V$
	ofcf.5	$⊢ φ \to C \in T$
Assertion	ofcf	$⊢ φ \to (F \circ_{fc} R C) : A ⟶ U$

Step	Hyp	Ref	Expression
1		ofcf.1	$⊢ (φ \land (x \in S \land y \in T)) \to x R y \in U$
2		ofcf.2	$⊢ φ \to F : A ⟶ S$
3		ofcf.4	$⊢ φ \to A \in V$
4		ofcf.5	$⊢ φ \to C \in T$
5	2	ffnd	$⊢ φ \to F Fn A$
6		eqidd	$⊢ (φ \land z \in A) \to F (z) = F (z)$
7	5 3 4 6	ofcfval	$⊢ φ \to F \circ_{fc} R C = (z \in A ⟼ F (z) R C)$
8	2	ffvelrnda	$⊢ (φ \land z \in A) \to F (z) \in S$
9	4	adantr	$⊢ (φ \land z \in A) \to C \in T$
10	1	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in T x R y \in U$
11	10	adantr	$⊢ (φ \land z \in A) \to \forall x \in S \forall y \in T x R y \in U$
12		ovrspc2v	$⊢ ((F (z) \in S \land C \in T) \land \forall x \in S \forall y \in T x R y \in U) \to F (z) R C \in U$
13	8 9 11 12	syl21anc	$⊢ (φ \land z \in A) \to F (z) R C \in U$
14	7 13	fmpt3d	$⊢ φ \to (F \circ_{fc} R C) : A ⟶ U$

Metamath Proof Explorer