offval2f

Description: The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 23-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		offval2f.0	$⊢ Ⅎ x φ$
2		offval2f.a	$⊢ \underline{Ⅎ} x A$
3		offval2f.1	$⊢ φ \to A \in V$
4		offval2f.2	$⊢ (φ \land x \in A) \to B \in W$
5		offval2f.3	$⊢ (φ \land x \in A) \to C \in X$
6		offval2f.4	$⊢ φ \to F = (x \in A ⟼ B)$
7		offval2f.5	$⊢ φ \to G = (x \in A ⟼ C)$
8	4	ex	$⊢ φ \to (x \in A \to B \in W)$
9	1 8	ralrimi	$⊢ φ \to \forall x \in A B \in W$
10	2	fnmptf	$⊢ \forall x \in A B \in W \to (x \in A ⟼ B) Fn A$
11	9 10	syl	$⊢ φ \to (x \in A ⟼ B) Fn A$
12	6	fneq1d	$⊢ φ \to (F Fn A \leftrightarrow (x \in A ⟼ B) Fn A)$
13	11 12	mpbird	$⊢ φ \to F Fn A$
14	5	ex	$⊢ φ \to (x \in A \to C \in X)$
15	1 14	ralrimi	$⊢ φ \to \forall x \in A C \in X$
16	2	fnmptf	$⊢ \forall x \in A C \in X \to (x \in A ⟼ C) Fn A$
17	15 16	syl	$⊢ φ \to (x \in A ⟼ C) Fn A$
18	7	fneq1d	$⊢ φ \to (G Fn A \leftrightarrow (x \in A ⟼ C) Fn A)$
19	17 18	mpbird	$⊢ φ \to G Fn A$
20		inidm	$⊢ A \cap A = A$
21	6	adantr	$⊢ (φ \land y \in A) \to F = (x \in A ⟼ B)$
22	21	fveq1d	$⊢ (φ \land y \in A) \to F (y) = (x \in A ⟼ B) (y)$
23	7	adantr	$⊢ (φ \land y \in A) \to G = (x \in A ⟼ C)$
24	23	fveq1d	$⊢ (φ \land y \in A) \to G (y) = (x \in A ⟼ C) (y)$
25	13 19 3 3 20 22 24	offval	$⊢ φ \to F R_{f} G = (y \in A ⟼ (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y))$
26		nfcv	$⊢ \underline{Ⅎ} y A$
27		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (y)$
28		nfcv	$⊢ \underline{Ⅎ} x R$
29		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C) (y)$
30	27 28 29	nfov	$⊢ \underline{Ⅎ} x ((x \in A ⟼ B) (y) R (x \in A ⟼ C) (y))$
31		nfcv	$⊢ \underline{Ⅎ} y ((x \in A ⟼ B) (x) R (x \in A ⟼ C) (x))$
32		fveq2	$⊢ y = x \to (x \in A ⟼ B) (y) = (x \in A ⟼ B) (x)$
33		fveq2	$⊢ y = x \to (x \in A ⟼ C) (y) = (x \in A ⟼ C) (x)$
34	32 33	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)$
35	26 2 30 31 34	cbvmptf	$⊢ (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))$
36		simpr	$⊢ (φ \land x \in A) \to x \in A$
37	2	fvmpt2f	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
38	36 4 37	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
39	2	fvmpt2f	$⊢ (x \in A \land C \in X) \to (x \in A ⟼ C) (x) = C$
40	36 5 39	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ C) (x) = C$
41	38 40	oveq12d	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x) = B R C$
42	1 41	mpteq2da	$⊢ φ \to (x \in A ⟼ (x \in A ⟼ B) (x) R (x \in A ⟼ C) (x)) = (x \in A ⟼ B R C)$
43	35 42	syl5eq	$⊢ φ \to (y \in A ⟼ (x \in A ⟼ B) (y) R (x \in A ⟼ C) (y)) = (x \in A ⟼ B R C)$
44	25 43	eqtrd	$⊢ φ \to F R_{f} G = (x \in A ⟼ B R C)$

Metamath Proof Explorer

Theorem offval2f

Proof