uncf1

Description: Value of the uncurry functor on an object. (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	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	uncf1	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑌 ) = ( ( 1^st ‘ ( ( 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	1 2 3 4	uncfval	⊢ ( 𝜑 → 𝐹 = ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) )
10	9	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) = ( 1^st ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) )
11	10	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑌 ) = ( 𝑋 ( 1^st ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) 𝑌 ) )
12		df-ov	⊢ ( 𝑋 ( 1^st ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) 𝑌 ) = ( ( 1^st ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
13		eqid	⊢ ( 𝐶 ×_c 𝐷 ) = ( 𝐶 ×_c 𝐷 )
14	13 5 6	xpcbas	⊢ ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×_c 𝐷 ) )
15		eqid	⊢ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) = ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) )
16		eqid	⊢ ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 ) = ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 )
17		funcrcl	⊢ ( 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
18	4 17	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
19	18	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
20		eqid	⊢ ( 𝐶 1^st_F 𝐷 ) = ( 𝐶 1^st_F 𝐷 )
21	13 19 2 20	1stfcl	⊢ ( 𝜑 → ( 𝐶 1^st_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐶 ) )
22	21 4	cofucl	⊢ ( 𝜑 → ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func ( 𝐷 FuncCat 𝐸 ) ) )
23		eqid	⊢ ( 𝐶 2^nd_F 𝐷 ) = ( 𝐶 2^nd_F 𝐷 )
24	13 19 2 23	2ndfcl	⊢ ( 𝜑 → ( 𝐶 2^nd_F 𝐷 ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func 𝐷 ) )
25	15 16 22 24	prfcl	⊢ ( 𝜑 → ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ∈ ( ( 𝐶 ×_c 𝐷 ) Func ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 ) ) )
26		eqid	⊢ ( 𝐷 eval_F 𝐸 ) = ( 𝐷 eval_F 𝐸 )
27		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
28	26 27 2 3	evlfcl	⊢ ( 𝜑 → ( 𝐷 eval_F 𝐸 ) ∈ ( ( ( 𝐷 FuncCat 𝐸 ) ×_c 𝐷 ) Func 𝐸 ) )
29	7 8	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × 𝐵 ) )
30	14 25 28 29	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) ‘ ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
31	12 30	syl5eq	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ ( ( 𝐷 eval_F 𝐸 ) ∘_func ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ) 𝑌 ) = ( ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) ‘ ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
32		eqid	⊢ ( Hom ‘ ( 𝐶 ×_c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×_c 𝐷 ) )
33	15 14 32 22 24 29	prf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) , ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ )
34	14 21 4 29	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )
35	13 14 32 19 2 20 29	1stf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
36		op1stg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
37	7 8 36	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
38	35 37	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑋 )
39	38	fveq2d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ ( 𝐶 1^st_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
40	34 39	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) )
41	13 14 32 19 2 23 29	2ndf1	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
42		op2ndg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
43	7 8 42	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
44	41 43	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = 𝑌 )
45	40 44	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) , ( ( 1^st ‘ ( 𝐶 2^nd_F 𝐷 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ⟩ = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ )
46	33 45	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ )
47	46	fveq2d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) ‘ ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ ) )
48		df-ov	⊢ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) 𝑌 ) = ( ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) ‘ ⟨ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 ⟩ )
49	47 48	eqtr4di	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) ‘ ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) 𝑌 ) )
50	27	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
51		relfunc	⊢ Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) )
52		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ∧ 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
53	51 4 52	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2^nd ‘ 𝐺 ) )
54	5 50 53	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐴 ⟶ ( 𝐷 Func 𝐸 ) )
55	54 7	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐸 ) )
56	26 2 3 6 55 8	evlf1	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) 𝑌 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) )
57	49 56	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐷 eval_F 𝐸 ) ) ‘ ( ( 1^st ‘ ( ( 𝐺 ∘_func ( 𝐶 1^st_F 𝐷 ) ) ⟨,⟩_F ( 𝐶 2^nd_F 𝐷 ) ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) )
58	11 31 57	3eqtrd	⊢ ( 𝜑 → ( 𝑋 ( 1^st ‘ 𝐹 ) 𝑌 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) )

Metamath Proof Explorer

Theorem uncf1

Proof