offval22

Description: The function operation expressed as a mapping, variation of offval2 . (Contributed by SO, 15-Jul-2018)

	Ref	Expression
Hypotheses	offval22.a	$⊢ φ \to A \in V$
	offval22.b	$⊢ φ \to B \in W$
	offval22.c	$⊢ (φ \land x \in A \land y \in B) \to C \in X$
	offval22.d	$⊢ (φ \land x \in A \land y \in B) \to D \in Y$
	offval22.f	$⊢ φ \to F = (x \in A, y \in B ⟼ C)$
	offval22.g	$⊢ φ \to G = (x \in A, y \in B ⟼ D)$
Assertion	offval22	$⊢ φ \to F R_{f} G = (x \in A, y \in B ⟼ C R D)$

Proof

Step	Hyp	Ref	Expression
1		offval22.a	$⊢ φ \to A \in V$
2		offval22.b	$⊢ φ \to B \in W$
3		offval22.c	$⊢ (φ \land x \in A \land y \in B) \to C \in X$
4		offval22.d	$⊢ (φ \land x \in A \land y \in B) \to D \in Y$
5		offval22.f	$⊢ φ \to F = (x \in A, y \in B ⟼ C)$
6		offval22.g	$⊢ φ \to G = (x \in A, y \in B ⟼ D)$
7	1 2	xpexd	$⊢ φ \to A \times B \in V$
8		xp1st	$⊢ z \in (A \times B) \to 1^{st} (z) \in A$
9		xp2nd	$⊢ z \in (A \times B) \to 2^{nd} (z) \in B$
10	8 9	jca	$⊢ z \in (A \times B) \to (1^{st} (z) \in A \land 2^{nd} (z) \in B)$
11		fvex	$⊢ 2^{nd} (z) \in V$
12		fvex	$⊢ 1^{st} (z) \in V$
13		nfcv	$⊢ \underline{Ⅎ} y 2^{nd} (z)$
14		nfcv	$⊢ \underline{Ⅎ} x 2^{nd} (z)$
15		nfcv	$⊢ \underline{Ⅎ} x 1^{st} (z)$
16		nfv	$⊢ Ⅎ y (φ \land x \in A \land 2^{nd} (z) \in B)$
17		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ 2^{nd} (z) / y ⦌ C$
18	17	nfel1	$⊢ Ⅎ y ⦋ 2^{nd} (z) / y ⦌ C \in V$
19	16 18	nfim	$⊢ Ⅎ y ((φ \land x \in A \land 2^{nd} (z) \in B) \to ⦋ 2^{nd} (z) / y ⦌ C \in V)$
20		nfv	$⊢ Ⅎ x (φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B)$
21		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C$
22	21	nfel1	$⊢ Ⅎ x ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V$
23	20 22	nfim	$⊢ Ⅎ x ((φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V)$
24		eleq1	$⊢ y = 2^{nd} (z) \to (y \in B \leftrightarrow 2^{nd} (z) \in B)$
25	24	3anbi3d	$⊢ y = 2^{nd} (z) \to ((φ \land x \in A \land y \in B) \leftrightarrow (φ \land x \in A \land 2^{nd} (z) \in B))$
26		csbeq1a	$⊢ y = 2^{nd} (z) \to C = ⦋ 2^{nd} (z) / y ⦌ C$
27	26	eleq1d	$⊢ y = 2^{nd} (z) \to (C \in V \leftrightarrow ⦋ 2^{nd} (z) / y ⦌ C \in V)$
28	25 27	imbi12d	$⊢ y = 2^{nd} (z) \to (((φ \land x \in A \land y \in B) \to C \in V) \leftrightarrow ((φ \land x \in A \land 2^{nd} (z) \in B) \to ⦋ 2^{nd} (z) / y ⦌ C \in V))$
29		eleq1	$⊢ x = 1^{st} (z) \to (x \in A \leftrightarrow 1^{st} (z) \in A)$
30	29	3anbi2d	$⊢ x = 1^{st} (z) \to ((φ \land x \in A \land 2^{nd} (z) \in B) \leftrightarrow (φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B))$
31		csbeq1a	$⊢ x = 1^{st} (z) \to ⦋ 2^{nd} (z) / y ⦌ C = ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C$
32	31	eleq1d	$⊢ x = 1^{st} (z) \to (⦋ 2^{nd} (z) / y ⦌ C \in V \leftrightarrow ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V)$
33	30 32	imbi12d	$⊢ x = 1^{st} (z) \to (((φ \land x \in A \land 2^{nd} (z) \in B) \to ⦋ 2^{nd} (z) / y ⦌ C \in V) \leftrightarrow ((φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V))$
34	3	elexd	$⊢ (φ \land x \in A \land y \in B) \to C \in V$
35	13 14 15 19 23 28 33 34	vtocl2gf	$⊢ (2^{nd} (z) \in V \land 1^{st} (z) \in V) \to ((φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V)$
36	11 12 35	mp2an	$⊢ (φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V$
37	36	3expb	$⊢ (φ \land (1^{st} (z) \in A \land 2^{nd} (z) \in B)) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V$
38	10 37	sylan2	$⊢ (φ \land z \in (A \times B)) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C \in V$
39		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ 2^{nd} (z) / y ⦌ D$
40	39	nfel1	$⊢ Ⅎ y ⦋ 2^{nd} (z) / y ⦌ D \in V$
41	16 40	nfim	$⊢ Ⅎ y ((φ \land x \in A \land 2^{nd} (z) \in B) \to ⦋ 2^{nd} (z) / y ⦌ D \in V)$
42		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D$
43	42	nfel1	$⊢ Ⅎ x ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V$
44	20 43	nfim	$⊢ Ⅎ x ((φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V)$
45		csbeq1a	$⊢ y = 2^{nd} (z) \to D = ⦋ 2^{nd} (z) / y ⦌ D$
46	45	eleq1d	$⊢ y = 2^{nd} (z) \to (D \in V \leftrightarrow ⦋ 2^{nd} (z) / y ⦌ D \in V)$
47	25 46	imbi12d	$⊢ y = 2^{nd} (z) \to (((φ \land x \in A \land y \in B) \to D \in V) \leftrightarrow ((φ \land x \in A \land 2^{nd} (z) \in B) \to ⦋ 2^{nd} (z) / y ⦌ D \in V))$
48		csbeq1a	$⊢ x = 1^{st} (z) \to ⦋ 2^{nd} (z) / y ⦌ D = ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D$
49	48	eleq1d	$⊢ x = 1^{st} (z) \to (⦋ 2^{nd} (z) / y ⦌ D \in V \leftrightarrow ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V)$
50	30 49	imbi12d	$⊢ x = 1^{st} (z) \to (((φ \land x \in A \land 2^{nd} (z) \in B) \to ⦋ 2^{nd} (z) / y ⦌ D \in V) \leftrightarrow ((φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V))$
51	4	elexd	$⊢ (φ \land x \in A \land y \in B) \to D \in V$
52	13 14 15 41 44 47 50 51	vtocl2gf	$⊢ (2^{nd} (z) \in V \land 1^{st} (z) \in V) \to ((φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V)$
53	11 12 52	mp2an	$⊢ (φ \land 1^{st} (z) \in A \land 2^{nd} (z) \in B) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V$
54	53	3expb	$⊢ (φ \land (1^{st} (z) \in A \land 2^{nd} (z) \in B)) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V$
55	10 54	sylan2	$⊢ (φ \land z \in (A \times B)) \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D \in V$
56		mpompts	$⊢ (x \in A, y \in B ⟼ C) = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C)$
57	5 56	eqtrdi	$⊢ φ \to F = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C)$
58		mpompts	$⊢ (x \in A, y \in B ⟼ D) = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D)$
59	6 58	eqtrdi	$⊢ φ \to G = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D)$
60	7 38 55 57 59	offval2	$⊢ φ \to F R_{f} G = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C R ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D)$
61		csbov12g	$⊢ 2^{nd} (z) \in V \to ⦋ 2^{nd} (z) / y ⦌ (C R D) = ⦋ 2^{nd} (z) / y ⦌ C R ⦋ 2^{nd} (z) / y ⦌ D$
62	61	csbeq2dv	$⊢ 2^{nd} (z) \in V \to ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ (C R D) = ⦋ 1^{st} (z) / x ⦌ (⦋ 2^{nd} (z) / y ⦌ C R ⦋ 2^{nd} (z) / y ⦌ D)$
63	11 62	ax-mp	$⊢ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ (C R D) = ⦋ 1^{st} (z) / x ⦌ (⦋ 2^{nd} (z) / y ⦌ C R ⦋ 2^{nd} (z) / y ⦌ D)$
64		csbov12g	$⊢ 1^{st} (z) \in V \to ⦋ 1^{st} (z) / x ⦌ (⦋ 2^{nd} (z) / y ⦌ C R ⦋ 2^{nd} (z) / y ⦌ D) = ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C R ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D$
65	12 64	ax-mp	$⊢ ⦋ 1^{st} (z) / x ⦌ (⦋ 2^{nd} (z) / y ⦌ C R ⦋ 2^{nd} (z) / y ⦌ D) = ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C R ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D$
66	63 65	eqtr2i	$⊢ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C R ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D = ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ (C R D)$
67	66	mpteq2i	$⊢ (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C R ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D) = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ (C R D))$
68		mpompts	$⊢ (x \in A, y \in B ⟼ C R D) = (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ (C R D))$
69	67 68	eqtr4i	$⊢ (z \in (A \times B) ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ C R ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ D) = (x \in A, y \in B ⟼ C R D)$
70	60 69	eqtrdi	$⊢ φ \to F R_{f} G = (x \in A, y \in B ⟼ C R D)$

Metamath Proof Explorer

Theorem offval22

Proof