uncf2

Description: Value of the uncurry functor on a morphism. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	uncfval.g	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 )
	uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
	uncf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	uncf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uncf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	uncf1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	uncf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	uncf2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	uncf2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
	uncf2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	uncf2.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑍 ) )
	uncf2.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑌 𝐽 𝑊 ) )
Assertion	uncf2	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑆 ) = ( ( ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) ‘ 𝑊 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑊 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ‘ 𝑊 ) ) ( ( 𝑌 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		uncfval.g	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurry_F 𝐺 )
2		uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
4		uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
5		uncf1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
6		uncf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
7		uncf1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8		uncf1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		uncf2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
10		uncf2.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
11		uncf2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐴 )
12		uncf2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
13		uncf2.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑍 ) )
14		uncf2.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑌 𝐽 𝑊 ) )
15	1 2 3 4	uncfval	⊢ ( 𝜑 → 𝐹 = ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) )
16	15	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) = ( 2^nd ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) )
17	16	oveqd	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) )
18	17	oveqd	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑆 ) = ( 𝑅 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑆 ) )
19		df-ov	⊢ ( 𝑅 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑆 ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ )
20		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
21	20 5 6	xpcbas	⊢ ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
22		eqid	⊢ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) = ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) )
23		eqid	⊢ ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 ) = ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 )
24		funcrcl	⊢ ( 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
25	4 24	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
26	25	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
27		eqid	⊢ ( 𝐶 1^st_F 𝐷 ) = ( 𝐶 1^st_F 𝐷 )
28	20 26 2 27	1stfcl	⊢ ( 𝜑 → ( 𝐶 1^st_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐶 ) )
29	28 4	cofucl	⊢ ( 𝜑 → ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func ( 𝐷 FuncCat 𝐸 ) ) )
30		eqid	⊢ ( 𝐶 2^nd_F 𝐷 ) = ( 𝐶 2^nd_F 𝐷 )
31	20 26 2 30	2ndfcl	⊢ ( 𝜑 → ( 𝐶 2^nd_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐷 ) )
32	22 23 29 31	prfcl	⊢ ( 𝜑 → ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 ) ) )
33		eqid	⊢ ( 𝐷 eval_F 𝐸 ) = ( 𝐷 eval_F 𝐸 )
34		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
35	33 34 2 3	evlfcl	⊢ ( 𝜑 → ( 𝐷 eval_F 𝐸 ) ∈ ( ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 ) Func 𝐸 ) )
36	7 8	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
37	11 12	opelxpd	⊢ ( 𝜑 → ⟨ 𝑍 , 𝑊 ⟩ ∈ ( 𝐴 × 𝐵 ) )
38		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
39	13 14	opelxpd	⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ( 𝑋 𝐻 𝑍 ) × ( 𝑌 𝐽 𝑊 ) ) )
40	20 5 6 9 10 7 8 11 12 38	xpchom2	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( ( 𝑋 𝐻 𝑍 ) × ( 𝑌 𝐽 𝑊 ) ) )
41	39 40	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) )
42	21 32 35 36 37 38 41	cofu2	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ( ( ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) )
43	19 42	syl5eq	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑆 ) = ( ( ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) )
44	18 43	eqtrd	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑆 ) = ( ( ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) )
45	22 21 38 29 31 36	prf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) , ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ )
46	21 28 4 36	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
47	20 21 38 26 2 27 36	1stf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
48		op1stg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
49	7 8 48	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
50	47 49	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
51	50	fveq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
52	46 51	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
53	20 21 38 26 2 30 36	2ndf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
54		op2ndg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
55	7 8 54	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
56	53 55	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
57	52 56	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) , ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ )
58	45 57	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ )
59	22 21 38 29 31 37	prf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) , ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ⟩ )
60	21 28 4 37	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) )
61	20 21 38 26 2 27 37	1stf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) )
62		op1stg	⊢ ( ( 𝑍 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
63	11 12 62	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
64	61 63	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑍 )
65	64	fveq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) )
66	60 65	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) )
67	20 21 38 26 2 30 37	2ndf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) )
68		op2ndg	⊢ ( ( 𝑍 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
69	11 12 68	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
70	67 69	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = 𝑊 )
71	66 70	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) , ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ )
72	59 71	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ )
73	58 72	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) = ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ ) )
74	22 21 38 29 31 36 37 41	prf2	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) , ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ⟩ )
75	21 28 4 36 37 38 41	cofu2	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ( ( ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 1^st_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) )
76	50 64	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) = ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) )
77	20 21 38 26 2 27 36 37	1stf2	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 1^st_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( 1^st ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ) )
78	77	fveq1d	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 1^st_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ( ( 1^st ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
79	41	fvresd	⊢ ( 𝜑 → ( ( 1^st ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ( 1^st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
80		op1stg	⊢ ( ( 𝑅 ∈ ( 𝑋 𝐻 𝑍 ) ∧ 𝑆 ∈ ( 𝑌 𝐽 𝑊 ) ) → ( 1^st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
81	13 14 80	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
82	78 79 81	3eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 1^st_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
83	76 82	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 1^st_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) = ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) )
84	75 83	eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) )
85	20 21 38 26 2 30 36 37	2ndf2	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( 2^nd ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ) )
86	85	fveq1d	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ( ( 2^nd ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
87	41	fvresd	⊢ ( 𝜑 → ( ( 2^nd ↾ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ( 2^nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) )
88		op2ndg	⊢ ( ( 𝑅 ∈ ( 𝑋 𝐻 𝑍 ) ∧ 𝑆 ∈ ( 𝑌 𝐽 𝑊 ) ) → ( 2^nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑆 )
89	13 14 88	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑆 )
90	86 87 89	3eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑆 )
91	84 90	opeq12d	⊢ ( 𝜑 → ⟨ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) , ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( 𝐶 2^nd_F 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ⟩ = ⟨ ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) , 𝑆 ⟩ )
92	74 91	eqtrd	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) , 𝑆 ⟩ )
93	73 92	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) = ( ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ ) ‘ ⟨ ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) , 𝑆 ⟩ ) )
94		df-ov	⊢ ( ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ ) 𝑆 ) = ( ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ ) ‘ ⟨ ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) , 𝑆 ⟩ )
95	93 94	eqtr4di	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑍 , 𝑊 ⟩ ) ) ‘ ( ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ ) 𝑆 ) )
96		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
97		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
98	34	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
99		relfunc	⊢ Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) )
100		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ∧ 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
101	99 4 100	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
102	5 98 101	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐴 ⟶ ( 𝐷 Func 𝐸 ) )
103	102 7	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐸 ) )
104	102 11	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ∈ ( 𝐷 Func 𝐸 ) )
105		eqid	⊢ ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ ) = ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ )
106	34 97	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
107	5 9 106 101 7 11	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) : ( 𝑋 𝐻 𝑍 ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
108	107 13	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 𝐷 Nat 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) )
109	33 2 3 6 10 96 97 103 104 8 12 105 108 14	evlf2val	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) ( ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ( 2^nd ‘ ( 𝐷 eval_F 𝐸 ) ) ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) , 𝑊 ⟩ ) 𝑆 ) = ( ( ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) ‘ 𝑊 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑊 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ‘ 𝑊 ) ) ( ( 𝑌 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝑆 ) ) )
110	44 95 109	3eqtrd	⊢ ( 𝜑 → ( 𝑅 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2^nd ‘ 𝐹 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝑆 ) = ( ( ( ( 𝑋 ( 2^nd ‘ 𝐺 ) 𝑍 ) ‘ 𝑅 ) ‘ 𝑊 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑊 ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑍 ) ) ‘ 𝑊 ) ) ( ( 𝑌 ( 2^nd ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) 𝑊 ) ‘ 𝑆 ) ) )

Metamath Proof Explorer

Theorem uncf2

Proof