offval2

Description: The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014)

	Ref	Expression
Hypotheses	offval2.1	$⊢ φ \to A \in V$
	offval2.2	$⊢ (φ \land x \in A) \to B \in W$
	offval2.3	$⊢ (φ \land x \in A) \to C \in X$
	offval2.4	$⊢ φ \to F = (x \in A ⟼ B)$
	offval2.5	$⊢ φ \to G = (x \in A ⟼ C)$
Assertion	offval2	$⊢ φ \to F R_{f} G = (x \in A ⟼ B R C)$

Proof

Step	Hyp	Ref	Expression
1		offval2.1	$⊢ φ \to A \in V$
2		offval2.2	$⊢ (φ \land x \in A) \to B \in W$
3		offval2.3	$⊢ (φ \land x \in A) \to C \in X$
4		offval2.4	$⊢ φ \to F = (x \in A ⟼ B)$
5		offval2.5	$⊢ φ \to G = (x \in A ⟼ C)$
6	2	ralrimiva	$⊢ φ \to \forall x \in A B \in W$
7		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
8	7	fnmpt	$⊢ \forall x \in A B \in W \to (x \in A ⟼ B) Fn A$
9	6 8	syl	$⊢ φ \to (x \in A ⟼ B) Fn A$
10	4	fneq1d	$⊢ φ \to (F Fn A \leftrightarrow (x \in A ⟼ B) Fn A)$
11	9 10	mpbird	$⊢ φ \to F Fn A$
12	3	ralrimiva	$⊢ φ \to \forall x \in A C \in X$
13		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
14	13	fnmpt	$⊢ \forall x \in A C \in X \to (x \in A ⟼ C) Fn A$
15	12 14	syl	$⊢ φ \to (x \in A ⟼ C) Fn A$
16	5	fneq1d	$⊢ φ \to (G Fn A \leftrightarrow (x \in A ⟼ C) Fn A)$
17	15 16	mpbird	$⊢ φ \to G Fn A$
18		inidm	$⊢ A \cap A = A$
19	4	adantr	$⊢ (φ \land y \in A) \to F = (x \in A ⟼ B)$
20	19	fveq1d	$⊢ (φ \land y \in A) \to F (y) = (x \in A ⟼ B) (y)$
21	5	adantr	$⊢ (φ \land y \in A) \to G = (x \in A ⟼ C)$
22	21	fveq1d	$⊢ (φ \land y \in A) \to G (y) = (x \in A ⟼ C) (y)$
23	11 17 1 1 18 20 22	offval	$⊢ φ \to F R_{f} G = (y \in A ⟼ (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y))$
24		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (y)$
25		nfcv	$⊢ \underline{Ⅎ} x R$
26		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C) (y)$
27	24 25 26	nfov	$⊢ \underline{Ⅎ} x ((x \in A ⟼ B) (y) R (x \in A ⟼ C) (y))$
28		nfcv	$⊢ \underline{Ⅎ} y ((x \in A ⟼ B) (x) R (x \in A ⟼ C) (x))$
29		fveq2	$⊢ y = x \to (x \in A ⟼ B) (y) = (x \in A ⟼ B) (x)$
30		fveq2	$⊢ y = x \to (x \in A ⟼ C) (y) = (x \in A ⟼ C) (x)$
31	29 30	oveq12d	$⊢ y = x \to (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y) = (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x)$
32	27 28 31	cbvmpt	$⊢ (y \in A ⟼ (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y)) = (x \in A ⟼ (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x))$
33		simpr	$⊢ (φ \land x \in A) \to x \in A$
34	7	fvmpt2	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
35	33 2 34	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
36	13	fvmpt2	$⊢ (x \in A \land C \in X) \to (x \in A ⟼ C) (x) = C$
37	33 3 36	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ C) (x) = C$
38	35 37	oveq12d	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x) = B R C$
39	38	mpteq2dva	$⊢ φ \to (x \in A ⟼ (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x)) = (x \in A ⟼ B R C)$
40	32 39	eqtrid	$⊢ φ \to (y \in A ⟼ (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y)) = (x \in A ⟼ B R C)$
41	23 40	eqtrd	$⊢ φ \to F R_{f} G = (x \in A ⟼ B R C)$

Metamath Proof Explorer

Theorem offval2

Proof