1st2ndprf

Description: Break a functor into a product category into first and second projections. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	1st2ndprf.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐸 )
	1st2ndprf.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝑇 ) )
	1st2ndprf.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	1st2ndprf.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
Assertion	1st2ndprf	⊢ ( 𝜑 → 𝐹 = ( ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ⟨,⟩_F ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1st2ndprf.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐸 )
2		1st2ndprf.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝑇 ) )
3		1st2ndprf.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		1st2ndprf.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8	1 6 7	xpcbas	⊢ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) = ( Base ‘ 𝑇 )
9		relfunc	⊢ Rel ( 𝐶 Func 𝑇 )
10		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑇 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝑇 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝑇 ) ( 2^nd ‘ 𝐹 ) )
11	9 2 10	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝑇 ) ( 2^nd ‘ 𝐹 ) )
12	5 8 11	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
13	12	feqmptd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
14	12	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
15		1st2nd2	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ )
16	14 15	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ )
17	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 ∈ ( 𝐶 Func 𝑇 ) )
18		eqid	⊢ ( 𝐷 1^st_F 𝐸 ) = ( 𝐷 1^st_F 𝐸 )
19	1 3 4 18	1stfcl	⊢ ( 𝜑 → ( 𝐷 1^st_F 𝐸 ) ∈ ( 𝑇 Func 𝐷 ) )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐷 1^st_F 𝐸 ) ∈ ( 𝑇 Func 𝐷 ) )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
22	5 17 20 21	cofu1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
23		eqid	⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
24	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
25	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
26	1 8 23 24 25 18 14	1stf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( 1^st ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
27	22 26	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( 1^st ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
28		eqid	⊢ ( 𝐷 2^nd_F 𝐸 ) = ( 𝐷 2^nd_F 𝐸 )
29	1 3 4 28	2ndfcl	⊢ ( 𝜑 → ( 𝐷 2^nd_F 𝐸 ) ∈ ( 𝑇 Func 𝐸 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐷 2^nd_F 𝐸 ) ∈ ( 𝑇 Func 𝐸 ) )
31	5 17 30 21	cofu1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝐷 2^nd_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
32	1 8 23 24 25 28 14	2ndf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝐷 2^nd_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( 2^nd ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
33	31 32	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( 2^nd ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
34	27 33	opeq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) ⟩ = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ )
35	16 34	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ⟨ ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) ⟩ )
36	35	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) ⟩ ) )
37	13 36	eqtrd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) ⟩ ) )
38	5 11	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
39		fnov	⊢ ( ( 2^nd ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2^nd ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
40	38 39	sylib	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
41		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
42	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝑇 ) ( 2^nd ‘ 𝐹 ) )
43		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
44		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
45	5 41 23 42 43 44	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
46	45	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
47	1 23	relxpchom	⊢ Rel ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) )
48	45	ffvelrnda	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
49		1st2nd	⊢ ( ( Rel ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∧ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) = ⟨ ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( 2^nd ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
50	47 48 49	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) = ⟨ ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( 2^nd ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
51	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐹 ∈ ( 𝐶 Func 𝑇 ) )
52	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝐷 1^st_F 𝐸 ) ∈ ( 𝑇 Func 𝐷 ) )
53	43	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
54	44	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
55		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
56	5 51 52 53 54 41 55	cofu2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
57	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐷 ∈ Cat )
58	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐸 ∈ Cat )
59	14	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
60	12	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
61	60	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
62	1 8 23 57 58 18 59 61	1stf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 1^st ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
63	62	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 1^st ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
64	63	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 1^st ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
65	48	fvresd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1^st ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
66	56 64 65	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) = ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
67	29	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 𝐷 2^nd_F 𝐸 ) ∈ ( 𝑇 Func 𝐸 ) )
68	5 51 67 53 54 41 55	cofu2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 2^nd_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
69	1 8 23 57 58 28 59 61	2ndf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 2^nd_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 2^nd ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
70	69	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 2^nd_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 2^nd ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
71	70	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 2^nd_F 𝐸 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 2^nd ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
72	48	fvresd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 2^nd ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( 2^nd ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
73	68 71 72	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) = ( 2^nd ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
74	66 73	opeq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ = ⟨ ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) , ( 2^nd ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) ⟩ )
75	50 74	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) = ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ )
76	75	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ ) )
77	46 76	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ ) )
78	77	3impb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ ) )
79	78	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ ) ) )
80	40 79	eqtrd	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ ) ) )
81	37 80	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ ) ) ⟩ )
82		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝑇 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝑇 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
83	9 2 82	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
84		eqid	⊢ ( ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ⟨,⟩_F ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) = ( ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ⟨,⟩_F ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) )
85	2 19	cofucl	⊢ ( 𝜑 → ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐷 ) )
86	2 29	cofucl	⊢ ( 𝜑 → ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
87	84 5 41 85 86	prfval	⊢ ( 𝜑 → ( ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ⟨,⟩_F ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) , ( ( 1^st ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) ⟩ ) ) ⟩ )
88	81 83 87	3eqtr4d	⊢ ( 𝜑 → 𝐹 = ( ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝐹 ) ⟨,⟩_F ( ( 𝐷 2^nd_F 𝐸 ) ∘_func 𝐹 ) ) )

Metamath Proof Explorer

Theorem 1st2ndprf

Proof