Theorem ixpovf

Description: A member of an indexed product of function spaces has the indicated function type at each pair of indices. Hom-functions of a functor are one application. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	ixpovf.p	|- ( ph -> P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) N ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
	ixpovf.u	|- ( ph -> U e. W )
	ixpovf.v	|- ( ph -> V e. W )
Assertion	ixpovf	|- ( ph -> ( U P V ) : ( U H V ) --> ( ( O ` U ) N ( O ` V ) ) )

Proof

Step	Hyp	Ref	Expression
1		ixpovf.p	|- ( ph -> P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) N ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) )
2		ixpovf.u	|- ( ph -> U e. W )
3		ixpovf.v	|- ( ph -> V e. W )
4	2 3	opelxpd	|- ( ph -> <. U , V >. e. ( W X. W ) )
5		2fveq3	|- ( z = <. U , V >. -> ( O ` ( 1st ` z ) ) = ( O ` ( 1st ` <. U , V >. ) ) )
6		2fveq3	|- ( z = <. U , V >. -> ( O ` ( 2nd ` z ) ) = ( O ` ( 2nd ` <. U , V >. ) ) )
7	5 6	oveq12d	|- ( z = <. U , V >. -> ( ( O ` ( 1st ` z ) ) N ( O ` ( 2nd ` z ) ) ) = ( ( O ` ( 1st ` <. U , V >. ) ) N ( O ` ( 2nd ` <. U , V >. ) ) ) )
8		fveq2	|- ( z = <. U , V >. -> ( H ` z ) = ( H ` <. U , V >. ) )
9	7 8	oveq12d	|- ( z = <. U , V >. -> ( ( ( O ` ( 1st ` z ) ) N ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( O ` ( 1st ` <. U , V >. ) ) N ( O ` ( 2nd ` <. U , V >. ) ) ) ^m ( H ` <. U , V >. ) ) )
10	9	fvixp	|- ( ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) N ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ <. U , V >. e. ( W X. W ) ) -> ( P ` <. U , V >. ) e. ( ( ( O ` ( 1st ` <. U , V >. ) ) N ( O ` ( 2nd ` <. U , V >. ) ) ) ^m ( H ` <. U , V >. ) ) )
11	1 4 10	syl2anc	|- ( ph -> ( P ` <. U , V >. ) e. ( ( ( O ` ( 1st ` <. U , V >. ) ) N ( O ` ( 2nd ` <. U , V >. ) ) ) ^m ( H ` <. U , V >. ) ) )
12	11	elmaprd	|- ( ph -> ( P ` <. U , V >. ) : ( H ` <. U , V >. ) --> ( ( O ` ( 1st ` <. U , V >. ) ) N ( O ` ( 2nd ` <. U , V >. ) ) ) )
13		df-ov	|- ( U P V ) = ( P ` <. U , V >. )
14	13	eqcomi	|- ( P ` <. U , V >. ) = ( U P V )
15	14	a1i	|- ( ph -> ( P ` <. U , V >. ) = ( U P V ) )
16		df-ov	|- ( U H V ) = ( H ` <. U , V >. )
17	16	eqcomi	|- ( H ` <. U , V >. ) = ( U H V )
18	17	a1i	|- ( ph -> ( H ` <. U , V >. ) = ( U H V ) )
19	2	elexd	|- ( ph -> U e. _V )
20	3	elexd	|- ( ph -> V e. _V )
21		op1stg	|- ( ( U e. _V /\ V e. _V ) -> ( 1st ` <. U , V >. ) = U )
22	19 20 21	syl2anc	|- ( ph -> ( 1st ` <. U , V >. ) = U )
23	22	fveq2d	|- ( ph -> ( O ` ( 1st ` <. U , V >. ) ) = ( O ` U ) )
24		op2ndg	|- ( ( U e. _V /\ V e. _V ) -> ( 2nd ` <. U , V >. ) = V )
25	19 20 24	syl2anc	|- ( ph -> ( 2nd ` <. U , V >. ) = V )
26	25	fveq2d	|- ( ph -> ( O ` ( 2nd ` <. U , V >. ) ) = ( O ` V ) )
27	23 26	oveq12d	|- ( ph -> ( ( O ` ( 1st ` <. U , V >. ) ) N ( O ` ( 2nd ` <. U , V >. ) ) ) = ( ( O ` U ) N ( O ` V ) ) )
28	15 18 27	feq123d	|- ( ph -> ( ( P ` <. U , V >. ) : ( H ` <. U , V >. ) --> ( ( O ` ( 1st ` <. U , V >. ) ) N ( O ` ( 2nd ` <. U , V >. ) ) ) <-> ( U P V ) : ( U H V ) --> ( ( O ` U ) N ( O ` V ) ) ) )
29	12 28	mpbid	|- ( ph -> ( U P V ) : ( U H V ) --> ( ( O ` U ) N ( O ` V ) ) )