Theorem imasubclem3

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

	Ref	Expression
Hypotheses	imasubclem1.f	$$⊢\phi \to F\in V$$
	imasubclem1.g	$$⊢\phi \to G\in W$$
	imasubclem3.x	$$⊢\phi \to X\in A$$
	imasubclem3.y	$$⊢\phi \to Y\in B$$
	imasubclem3.k	$$⊢K=\left(x\in A,y\in B⟼\bigcup _{z\in F^{-1}\left[\left\{x\right\}\right]\times G^{-1}\left[\left\{y\right\}\right]}H\left(C\right)\left[D\right]\right)$$
Assertion	imasubclem3	$$⊢\phi \to XKY=\bigcup _{z\in F^{-1}\left[\left\{X\right\}\right]\times G^{-1}\left[\left\{Y\right\}\right]}H\left(C\right)\left[D\right]$$

Proof

Step	Hyp	Ref	Expression
1		imasubclem1.f	$$⊢\phi \to F\in V$$
2		imasubclem1.g	$$⊢\phi \to G\in W$$
3		imasubclem3.x	$$⊢\phi \to X\in A$$
4		imasubclem3.y	$$⊢\phi \to Y\in B$$
5		imasubclem3.k	$$⊢K=\left(x\in A,y\in B⟼\bigcup _{z\in F^{-1}\left[\left\{x\right\}\right]\times G^{-1}\left[\left\{y\right\}\right]}H\left(C\right)\left[D\right]\right)$$
6	1 2	imasubclem1	$$⊢\phi \to \bigcup _{z\in F^{-1}\left[\left\{X\right\}\right]\times G^{-1}\left[\left\{Y\right\}\right]}H\left(C\right)\left[D\right]\in \mathrm{V}$$
7		simpl	$$⊢\left(x=X\wedge y=Y\right)\to x=X$$
8	7	sneqd	$$⊢\left(x=X\wedge y=Y\right)\to \left\{x\right\}=\left\{X\right\}$$
9	8	imaeq2d	$$⊢\left(x=X\wedge y=Y\right)\to F^{-1}\left[\left\{x\right\}\right]=F^{-1}\left[\left\{X\right\}\right]$$
10		simpr	$$⊢\left(x=X\wedge y=Y\right)\to y=Y$$
11	10	sneqd	$$⊢\left(x=X\wedge y=Y\right)\to \left\{y\right\}=\left\{Y\right\}$$
12	11	imaeq2d	$$⊢\left(x=X\wedge y=Y\right)\to G^{-1}\left[\left\{y\right\}\right]=G^{-1}\left[\left\{Y\right\}\right]$$
13	9 12	xpeq12d	$$⊢\left(x=X\wedge y=Y\right)\to F^{-1}\left[\left\{x\right\}\right]\times G^{-1}\left[\left\{y\right\}\right]=F^{-1}\left[\left\{X\right\}\right]\times G^{-1}\left[\left\{Y\right\}\right]$$
14	13	iuneq1d	$$⊢\left(x=X\wedge y=Y\right)\to \bigcup _{z\in F^{-1}\left[\left\{x\right\}\right]\times G^{-1}\left[\left\{y\right\}\right]}H\left(C\right)\left[D\right]=\bigcup _{z\in F^{-1}\left[\left\{X\right\}\right]\times G^{-1}\left[\left\{Y\right\}\right]}H\left(C\right)\left[D\right]$$
15	14 5	ovmpoga	$$⊢\left(X\in A\wedge Y\in B\wedge \bigcup _{z\in F^{-1}\left[\left\{X\right\}\right]\times G^{-1}\left[\left\{Y\right\}\right]}H\left(C\right)\left[D\right]\in \mathrm{V}\right)\to XKY=\bigcup _{z\in F^{-1}\left[\left\{X\right\}\right]\times G^{-1}\left[\left\{Y\right\}\right]}H\left(C\right)\left[D\right]$$
16	3 4 6 15	syl3anc	$$⊢\phi \to XKY=\bigcup _{z\in F^{-1}\left[\left\{X\right\}\right]\times G^{-1}\left[\left\{Y\right\}\right]}H\left(C\right)\left[D\right]$$