Theorem imasubclem2

Description: Lemma for imasubc . (Contributed by Zhi Wang, 7-Nov-2025)

	Ref	Expression
Hypotheses	imasubclem1.f	|- ( ph -> F e. V )
	imasubclem1.g	|- ( ph -> G e. W )
	imasubclem2.k	|- K = ( y e. X , z e. Y |-> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) )
Assertion	imasubclem2	|- ( ph -> K Fn ( X X. Y ) )

Proof

Step	Hyp	Ref	Expression
1		imasubclem1.f	|- ( ph -> F e. V )
2		imasubclem1.g	|- ( ph -> G e. W )
3		imasubclem2.k	|- K = ( y e. X , z e. Y |-> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) )
4	1 2	imasubclem1	|- ( ph -> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V )
5	4	adantr	|- ( ( ph /\ ( y e. X /\ z e. Y ) ) -> U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V )
6	5	ralrimivva	|- ( ph -> A. y e. X A. z e. Y U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V )
7	3	fnmpo	|- ( A. y e. X A. z e. Y U_ x e. ( ( `' F " A ) X. ( `' G " B ) ) ( ( H ` C ) " D ) e. _V -> K Fn ( X X. Y ) )
8	6 7	syl	|- ( ph -> K Fn ( X X. Y ) )