offval22

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

	Ref	Expression
Hypotheses	offval22.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offval22.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	offval22.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑋 )
	offval22.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝑌 )
	offval22.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
	offval22.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) )
Assertion	offval22	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		offval22.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		offval22.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		offval22.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑋 )
4		offval22.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ 𝑌 )
5		offval22.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
6		offval22.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) )
7	1 2	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
8		xp1st	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 1^st ‘ 𝑧 ) ∈ 𝐴 )
9		xp2nd	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 2^nd ‘ 𝑧 ) ∈ 𝐵 )
10	8 9	jca	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) )
11		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
12		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
13		nfcv	⊢ Ⅎ 𝑦 ( 2^nd ‘ 𝑧 )
14		nfcv	⊢ Ⅎ 𝑥 ( 2^nd ‘ 𝑧 )
15		nfcv	⊢ Ⅎ 𝑥 ( 1^st ‘ 𝑧 )
16		nfv	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 )
17		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶
18	17	nfel1	⊢ Ⅎ 𝑦 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V
19	16 18	nfim	⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V )
20		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 )
21		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶
22	21	nfel1	⊢ Ⅎ 𝑥 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V
23	20 22	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V )
24		eleq1	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( 𝑦 ∈ 𝐵 ↔ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) )
25	24	3anbi3d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) ) )
26		csbeq1a	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → 𝐶 = ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
27	26	eleq1d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( 𝐶 ∈ V ↔ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) )
28	25 27	imbi12d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ V ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ) )
29		eleq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( 𝑥 ∈ 𝐴 ↔ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ) )
30	29	3anbi2d	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) ↔ ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) ) )
31		csbeq1a	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
32	31	eleq1d	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ↔ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) )
33	30 32	imbi12d	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ↔ ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ) )
34	3	elexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ V )
35	13 14 15 19 23 28 33 34	vtocl2gf	⊢ ( ( ( 2^nd ‘ 𝑧 ) ∈ V ∧ ( 1^st ‘ 𝑧 ) ∈ V ) → ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) )
36	11 12 35	mp2an	⊢ ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V )
37	36	3expb	⊢ ( ( 𝜑 ∧ ( ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V )
38	10 37	sylan2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × 𝐵 ) ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V )
39		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷
40	39	nfel1	⊢ Ⅎ 𝑦 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V
41	16 40	nfim	⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V )
42		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷
43	42	nfel1	⊢ Ⅎ 𝑥 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V
44	20 43	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V )
45		csbeq1a	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → 𝐷 = ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 )
46	45	eleq1d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( 𝐷 ∈ V ↔ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) )
47	25 46	imbi12d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ V ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ) )
48		csbeq1a	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 = ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 )
49	48	eleq1d	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ↔ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) )
50	30 49	imbi12d	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ↔ ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ) )
51	4	elexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ V )
52	13 14 15 41 44 47 50 51	vtocl2gf	⊢ ( ( ( 2^nd ‘ 𝑧 ) ∈ V ∧ ( 1^st ‘ 𝑧 ) ∈ V ) → ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) )
53	11 12 52	mp2an	⊢ ( ( 𝜑 ∧ ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V )
54	53	3expb	⊢ ( ( 𝜑 ∧ ( ( 1^st ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V )
55	10 54	sylan2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × 𝐵 ) ) → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V )
56		mpompts	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
57	5 56	eqtrdi	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) )
58		mpompts	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 )
59	6 58	eqtrdi	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) )
60	7 38 55 57 59	offval2	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) )
61		csbov12g	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ V → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) = ( ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) )
62	61	csbeq2dv	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ V → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) = ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) )
63	11 62	ax-mp	⊢ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) = ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 )
64		csbov12g	⊢ ( ( 1^st ‘ 𝑧 ) ∈ V → ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) = ( ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) )
65	12 64	ax-mp	⊢ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) = ( ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 )
66	63 65	eqtr2i	⊢ ( ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) = ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 )
67	66	mpteq2i	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) )
68		mpompts	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) )
69	67 68	eqtr4i	⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑅 𝐷 ) )
70	60 69	eqtrdi	⊢ ( 𝜑 → ( 𝐹 ∘_f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) )

Metamath Proof Explorer

Theorem offval22

Proof