ofcfval

Description: Value of an operation applied to a function and a constant. (Contributed by Thierry Arnoux, 30-Jan-2017)

Step	Hyp	Ref	Expression
1		ofcfval.1	$⊢ φ \to F Fn A$
2		ofcfval.2	$⊢ φ \to A \in V$
3		ofcfval.3	$⊢ φ \to C \in W$
4		ofcfval.6	$⊢ (φ \land x \in A) \to F (x) = B$
5		df-ofc	$⊢ \circ_{fc} R = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c))$
6	5	a1i	$⊢ φ \to \circ_{fc} R = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c))$
7		simprl	$⊢ (φ \land (f = F \land c = C)) \to f = F$
8	7	dmeqd	$⊢ (φ \land (f = F \land c = C)) \to dom f = dom F$
9	7	fveq1d	$⊢ (φ \land (f = F \land c = C)) \to f (x) = F (x)$
10		simprr	$⊢ (φ \land (f = F \land c = C)) \to c = C$
11	9 10	oveq12d	$⊢ (φ \land (f = F \land c = C)) \to f (x) R c = F (x) R C$
12	8 11	mpteq12dv	$⊢ (φ \land (f = F \land c = C)) \to (x \in dom f ⟼ f (x) R c) = (x \in dom F ⟼ F (x) R C)$
13		fnex	$⊢ (F Fn A \land A \in V) \to F \in V$
14	1 2 13	syl2anc	$⊢ φ \to F \in V$
15	3	elexd	$⊢ φ \to C \in V$
16	1	fndmd	$⊢ φ \to dom F = A$
17	16 2	eqeltrd	$⊢ φ \to dom F \in V$
18	17	mptexd	$⊢ φ \to (x \in dom F ⟼ F (x) R C) \in V$
19	6 12 14 15 18	ovmpod	$⊢ φ \to F \circ_{fc} R C = (x \in dom F ⟼ F (x) R C)$
20	16	eleq2d	$⊢ φ \to (x \in dom F \leftrightarrow x \in A)$
21	20	pm5.32i	$⊢ (φ \land x \in dom F) \leftrightarrow (φ \land x \in A)$
22	21 4	sylbi	$⊢ (φ \land x \in dom F) \to F (x) = B$
23	22	oveq1d	$⊢ (φ \land x \in dom F) \to F (x) R C = B R C$
24	16 23	mpteq12dva	$⊢ φ \to (x \in dom F ⟼ F (x) R C) = (x \in A ⟼ B R C)$
25	19 24	eqtrd	$⊢ φ \to F \circ_{fc} R C = (x \in A ⟼ B R C)$

Metamath Proof Explorer