Theorem imasubclem3

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 )
	imasubclem3.x	|- ( ph -> X e. A )
	imasubclem3.y	|- ( ph -> Y e. B )
	imasubclem3.k	|- K = ( x e. A , y e. B |-> U_ z e. ( ( `' F " { x } ) X. ( `' G " { y } ) ) ( ( H ` C ) " D ) )
Assertion	imasubclem3	|- ( ph -> ( X K Y ) = U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) )

Proof

Step	Hyp	Ref	Expression
1		imasubclem1.f	|- ( ph -> F e. V )
2		imasubclem1.g	|- ( ph -> G e. W )
3		imasubclem3.x	|- ( ph -> X e. A )
4		imasubclem3.y	|- ( ph -> Y e. B )
5		imasubclem3.k	|- K = ( x e. A , y e. B |-> U_ z e. ( ( `' F " { x } ) X. ( `' G " { y } ) ) ( ( H ` C ) " D ) )
6	1 2	imasubclem1	|- ( ph -> U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) e. _V )
7		simpl	|- ( ( x = X /\ y = Y ) -> x = X )
8	7	sneqd	|- ( ( x = X /\ y = Y ) -> { x } = { X } )
9	8	imaeq2d	|- ( ( x = X /\ y = Y ) -> ( `' F " { x } ) = ( `' F " { X } ) )
10		simpr	|- ( ( x = X /\ y = Y ) -> y = Y )
11	10	sneqd	|- ( ( x = X /\ y = Y ) -> { y } = { Y } )
12	11	imaeq2d	|- ( ( x = X /\ y = Y ) -> ( `' G " { y } ) = ( `' G " { Y } ) )
13	9 12	xpeq12d	|- ( ( x = X /\ y = Y ) -> ( ( `' F " { x } ) X. ( `' G " { y } ) ) = ( ( `' F " { X } ) X. ( `' G " { Y } ) ) )
14	13	iuneq1d	|- ( ( x = X /\ y = Y ) -> U_ z e. ( ( `' F " { x } ) X. ( `' G " { y } ) ) ( ( H ` C ) " D ) = U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) )
15	14 5	ovmpoga	|- ( ( X e. A /\ Y e. B /\ U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) e. _V ) -> ( X K Y ) = U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) )
16	3 4 6 15	syl3anc	|- ( ph -> ( X K Y ) = U_ z e. ( ( `' F " { X } ) X. ( `' G " { Y } ) ) ( ( H ` C ) " D ) )