Theorem imasubc3lem2

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

	Ref	Expression
Hypotheses	imasubc3lem1.s	$$⊢S=F\left[A\right]$$
	imasubc3lem1.f	$$⊢\phi \to F:B\underset{1-1}{⟶}C$$
	imasubc3lem1.x	$$⊢\phi \to X\in S$$
	imasubc3lem2.y	$$⊢\phi \to Y\in S$$
	imasubc3lem2.f	$$⊢\phi \to F\in V$$
	imasubc3lem2.k	$$⊢K=\left(x\in S,y\in S⟼\bigcup _{p\in F^{-1}\left[\left\{x\right\}\right]\times F^{-1}\left[\left\{y\right\}\right]}G\left(p\right)\left[H\left(p\right)\right]\right)$$
Assertion	imasubc3lem2	$$⊢\phi \to XKY=\left(F^{-1}\left(X\right)G{F}^{-1}\left(Y\right)\right)\left[F^{-1}\left(X\right)H{F}^{-1}\left(Y\right)\right]$$

Proof

Step	Hyp	Ref	Expression
1		imasubc3lem1.s	$$⊢S=F\left[A\right]$$
2		imasubc3lem1.f	$$⊢\phi \to F:B\underset{1-1}{⟶}C$$
3		imasubc3lem1.x	$$⊢\phi \to X\in S$$
4		imasubc3lem2.y	$$⊢\phi \to Y\in S$$
5		imasubc3lem2.f	$$⊢\phi \to F\in V$$
6		imasubc3lem2.k	$$⊢K=\left(x\in S,y\in S⟼\bigcup _{p\in F^{-1}\left[\left\{x\right\}\right]\times F^{-1}\left[\left\{y\right\}\right]}G\left(p\right)\left[H\left(p\right)\right]\right)$$
7	5 5 3 4 6	imasubclem3	$$⊢\phi \to XKY=\bigcup _{p\in F^{-1}\left[\left\{X\right\}\right]\times F^{-1}\left[\left\{Y\right\}\right]}G\left(p\right)\left[H\left(p\right)\right]$$
8	1 2 3	imasubc3lem1	$$⊢\phi \to \left(\left\{F^{-1}\left(X\right)\right\}=F^{-1}\left[\left\{X\right\}\right]\wedge F\left(F^{-1}\left(X\right)\right)=X\wedge F^{-1}\left(X\right)\in B\right)$$
9	8	simp1d	$$⊢\phi \to \left\{F^{-1}\left(X\right)\right\}=F^{-1}\left[\left\{X\right\}\right]$$
10	1 2 4	imasubc3lem1	$$⊢\phi \to \left(\left\{F^{-1}\left(Y\right)\right\}=F^{-1}\left[\left\{Y\right\}\right]\wedge F\left(F^{-1}\left(Y\right)\right)=Y\wedge F^{-1}\left(Y\right)\in B\right)$$
11	10	simp1d	$$⊢\phi \to \left\{F^{-1}\left(Y\right)\right\}=F^{-1}\left[\left\{Y\right\}\right]$$
12	9 11	xpeq12d	$$⊢\phi \to \left\{F^{-1}\left(X\right)\right\}\times \left\{F^{-1}\left(Y\right)\right\}=F^{-1}\left[\left\{X\right\}\right]\times F^{-1}\left[\left\{Y\right\}\right]$$
13		fvex	$$⊢F^{-1}\left(X\right)\in \mathrm{V}$$
14		fvex	$$⊢F^{-1}\left(Y\right)\in \mathrm{V}$$
15	13 14	xpsn	$$⊢\left\{F^{-1}\left(X\right)\right\}\times \left\{F^{-1}\left(Y\right)\right\}=\left\{⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right\}$$
16	12 15	eqtr3di	$$⊢\phi \to F^{-1}\left[\left\{X\right\}\right]\times F^{-1}\left[\left\{Y\right\}\right]=\left\{⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right\}$$
17	16	iuneq1d	$$⊢\phi \to \bigcup _{p\in F^{-1}\left[\left\{X\right\}\right]\times F^{-1}\left[\left\{Y\right\}\right]}G\left(p\right)\left[H\left(p\right)\right]=\bigcup _{p\in \left\{⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right\}}G\left(p\right)\left[H\left(p\right)\right]$$
18	7 17	eqtrd	$$⊢\phi \to XKY=\bigcup _{p\in \left\{⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right\}}G\left(p\right)\left[H\left(p\right)\right]$$
19		opex	$$⊢⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\in \mathrm{V}$$
20		fveq2	$$⊢p=⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\to G\left(p\right)=G\left(⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right)$$
21		df-ov	$$⊢F^{-1}\left(X\right)G{F}^{-1}\left(Y\right)=G\left(⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right)$$
22	20 21	eqtr4di	$$⊢p=⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\to G\left(p\right)=F^{-1}\left(X\right)G{F}^{-1}\left(Y\right)$$
23		fveq2	$$⊢p=⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\to H\left(p\right)=H\left(⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right)$$
24		df-ov	$$⊢F^{-1}\left(X\right)H{F}^{-1}\left(Y\right)=H\left(⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right)$$
25	23 24	eqtr4di	$$⊢p=⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\to H\left(p\right)=F^{-1}\left(X\right)H{F}^{-1}\left(Y\right)$$
26	22 25	imaeq12d	$$⊢p=⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\to G\left(p\right)\left[H\left(p\right)\right]=\left(F^{-1}\left(X\right)G{F}^{-1}\left(Y\right)\right)\left[F^{-1}\left(X\right)H{F}^{-1}\left(Y\right)\right]$$
27	19 26	iunxsn	$$⊢\bigcup _{p\in \left\{⟨F^{-1}\left(X\right),F^{-1}\left(Y\right)⟩\right\}}G\left(p\right)\left[H\left(p\right)\right]=\left(F^{-1}\left(X\right)G{F}^{-1}\left(Y\right)\right)\left[F^{-1}\left(X\right)H{F}^{-1}\left(Y\right)\right]$$
28	18 27	eqtrdi	$$⊢\phi \to XKY=\left(F^{-1}\left(X\right)G{F}^{-1}\left(Y\right)\right)\left[F^{-1}\left(X\right)H{F}^{-1}\left(Y\right)\right]$$