ofcfval3

Description: General value of ( F oFC R C ) with no assumptions on functionality of F . (Contributed by Thierry Arnoux, 31-Jan-2017)

		Ref	Expression
	Assertion	ofcfval3	$⊢ (F \in V \land C \in W) \to F \circ_{fc} R C = (x \in dom F ⟼ F (x) R C)$

Step	Hyp	Ref	Expression
1		elex	$⊢ F \in V \to F \in V$
2	1	adantr	$⊢ (F \in V \land C \in W) \to F \in V$
3		elex	$⊢ C \in W \to C \in V$
4	3	adantl	$⊢ (F \in V \land C \in W) \to C \in V$
5		dmexg	$⊢ F \in V \to dom F \in V$
6		mptexg	$⊢ dom F \in V \to (x \in dom F ⟼ F (x) R C) \in V$
7	5 6	syl	$⊢ F \in V \to (x \in dom F ⟼ F (x) R C) \in V$
8	7	adantr	$⊢ (F \in V \land C \in W) \to (x \in dom F ⟼ F (x) R C) \in V$
9		simpl	$⊢ (f = F \land c = C) \to f = F$
10	9	dmeqd	$⊢ (f = F \land c = C) \to dom f = dom F$
11	9	fveq1d	$⊢ (f = F \land c = C) \to f (x) = F (x)$
12		simpr	$⊢ (f = F \land c = C) \to c = C$
13	11 12	oveq12d	$⊢ (f = F \land c = C) \to f (x) R c = F (x) R C$
14	10 13	mpteq12dv	$⊢ (f = F \land c = C) \to (x \in dom f ⟼ f (x) R c) = (x \in dom F ⟼ F (x) R C)$
15		df-ofc	$⊢ \circ_{fc} R = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c))$
16	14 15	ovmpoga	$⊢ (F \in V \land C \in V \land (x \in dom F ⟼ F (x) R C) \in V) \to F \circ_{fc} R C = (x \in dom F ⟼ F (x) R C)$
17	2 4 8 16	syl3anc	$⊢ (F \in V \land C \in W) \to F \circ_{fc} R C = (x \in dom F ⟼ F (x) R C)$

Metamath Proof Explorer