ofmpteq

Description: Value of a pointwise operation on two functions defined using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014)

		Ref	Expression
	Assertion	ofmpteq	$⊢ (A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \to (x \in A ⟼ B) R_{f} (x \in A ⟼ C) = (x \in A ⟼ B R C)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \to A \in V$
2		simpr	$⊢ ((A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \land a \in A) \to a \in A$
3		simpl2	$⊢ ((A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \land a \in A) \to (x \in A ⟼ B) Fn A$
4		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
5	4	mptfng	$⊢ \forall x \in A B \in V \leftrightarrow (x \in A ⟼ B) Fn A$
6	3 5	sylibr	$⊢ ((A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \land a \in A) \to \forall x \in A B \in V$
7		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ B$
8	7	nfel1	$⊢ Ⅎ x ⦋ a / x ⦌ B \in V$
9		csbeq1a	$⊢ x = a \to B = ⦋ a / x ⦌ B$
10	9	eleq1d	$⊢ x = a \to (B \in V \leftrightarrow ⦋ a / x ⦌ B \in V)$
11	8 10	rspc	$⊢ a \in A \to (\forall x \in A B \in V \to ⦋ a / x ⦌ B \in V)$
12	2 6 11	sylc	$⊢ ((A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \land a \in A) \to ⦋ a / x ⦌ B \in V$
13		simpl3	$⊢ ((A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \land a \in A) \to (x \in A ⟼ C) Fn A$
14		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
15	14	mptfng	$⊢ \forall x \in A C \in V \leftrightarrow (x \in A ⟼ C) Fn A$
16	13 15	sylibr	$⊢ ((A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \land a \in A) \to \forall x \in A C \in V$
17		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ C$
18	17	nfel1	$⊢ Ⅎ x ⦋ a / x ⦌ C \in V$
19		csbeq1a	$⊢ x = a \to C = ⦋ a / x ⦌ C$
20	19	eleq1d	$⊢ x = a \to (C \in V \leftrightarrow ⦋ a / x ⦌ C \in V)$
21	18 20	rspc	$⊢ a \in A \to (\forall x \in A C \in V \to ⦋ a / x ⦌ C \in V)$
22	2 16 21	sylc	$⊢ ((A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \land a \in A) \to ⦋ a / x ⦌ C \in V$
23		nfcv	$⊢ \underline{Ⅎ} a B$
24	23 7 9	cbvmpt	$⊢ (x \in A ⟼ B) = (a \in A ⟼ ⦋ a / x ⦌ B)$
25	24	a1i	$⊢ (A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \to (x \in A ⟼ B) = (a \in A ⟼ ⦋ a / x ⦌ B)$
26		nfcv	$⊢ \underline{Ⅎ} a C$
27	26 17 19	cbvmpt	$⊢ (x \in A ⟼ C) = (a \in A ⟼ ⦋ a / x ⦌ C)$
28	27	a1i	$⊢ (A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \to (x \in A ⟼ C) = (a \in A ⟼ ⦋ a / x ⦌ C)$
29	1 12 22 25 28	offval2	$⊢ (A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \to (x \in A ⟼ B) R_{f} (x \in A ⟼ C) = (a \in A ⟼ ⦋ a / x ⦌ B R ⦋ a / x ⦌ C)$
30		nfcv	$⊢ \underline{Ⅎ} a (B R C)$
31		nfcv	$⊢ \underline{Ⅎ} x R$
32	7 31 17	nfov	$⊢ \underline{Ⅎ} x (⦋ a / x ⦌ B R ⦋ a / x ⦌ C)$
33	9 19	oveq12d	$⊢ x = a \to B R C = ⦋ a / x ⦌ B R ⦋ a / x ⦌ C$
34	30 32 33	cbvmpt	$⊢ (x \in A ⟼ B R C) = (a \in A ⟼ ⦋ a / x ⦌ B R ⦋ a / x ⦌ C)$
35	29 34	eqtr4di	$⊢ (A \in V \land (x \in A ⟼ B) Fn A \land (x \in A ⟼ C) Fn A) \to (x \in A ⟼ B) R_{f} (x \in A ⟼ C) = (x \in A ⟼ B R C)$

Metamath Proof Explorer

Theorem ofmpteq

Proof