Theorem prdsvallem

Description: Lemma for prdsval . (Contributed by Stefan O'Rear, 3-Jan-2015) Extracted from the former proof of prdsval , dependency on df-hom removed. (Revised by AV, 13-Oct-2024)

	Ref	Expression
Assertion	prdsvallem	$$⊢\left(f\in v,g\in v⟼\underset{x\in \mathrm{dom}r}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\right)\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢v\in \mathrm{V}$$
2		ovex	$$⊢{\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r}^{\mathrm{dom}r}\in \mathrm{V}$$
3	2	pwex	$$⊢𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r}^{\mathrm{dom}r}\right)\in \mathrm{V}$$
4		ovssunirn	$$⊢f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\subseteq \bigcup \mathrm{ran}\mathrm{Hom}\left(r\left(x\right)\right)$$
5		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
6	5	strfvss	$$⊢\mathrm{Hom}\left(r\left(x\right)\right)\subseteq \bigcup \mathrm{ran}r\left(x\right)$$
7		fvssunirn	$$⊢r\left(x\right)\subseteq \bigcup \mathrm{ran}r$$
8		rnss	$$⊢r\left(x\right)\subseteq \bigcup \mathrm{ran}r\to \mathrm{ran}r\left(x\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}r$$
9		uniss	$$⊢\mathrm{ran}r\left(x\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}r\to \bigcup \mathrm{ran}r\left(x\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
10	7 8 9	mp2b	$$⊢\bigcup \mathrm{ran}r\left(x\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
11	6 10	sstri	$$⊢\mathrm{Hom}\left(r\left(x\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
12		rnss	$$⊢\mathrm{Hom}\left(r\left(x\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}r\to \mathrm{ran}\mathrm{Hom}\left(r\left(x\right)\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
13		uniss	$$⊢\mathrm{ran}\mathrm{Hom}\left(r\left(x\right)\right)\subseteq \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r\to \bigcup \mathrm{ran}\mathrm{Hom}\left(r\left(x\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
14	11 12 13	mp2b	$$⊢\bigcup \mathrm{ran}\mathrm{Hom}\left(r\left(x\right)\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
15	4 14	sstri	$$⊢f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
16	15	rgenw	$$⊢\forall x\in \mathrm{dom}rf\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
17		ss2ixp	$$⊢\forall x\in \mathrm{dom}rf\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\subseteq \bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r\to \underset{x\in \mathrm{dom}r}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\right)\subseteq \underset{x\in \mathrm{dom}r}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
18	16 17	ax-mp	$$⊢\underset{x\in \mathrm{dom}r}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\right)\subseteq \underset{x\in \mathrm{dom}r}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r$$
19		vex	$$⊢r\in \mathrm{V}$$
20	19	dmex	$$⊢\mathrm{dom}r\in \mathrm{V}$$
21	19	rnex	$$⊢\mathrm{ran}r\in \mathrm{V}$$
22	21	uniex	$$⊢\bigcup \mathrm{ran}r\in \mathrm{V}$$
23	22	rnex	$$⊢\mathrm{ran}\bigcup \mathrm{ran}r\in \mathrm{V}$$
24	23	uniex	$$⊢\bigcup \mathrm{ran}\bigcup \mathrm{ran}r\in \mathrm{V}$$
25	24	rnex	$$⊢\mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r\in \mathrm{V}$$
26	25	uniex	$$⊢\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r\in \mathrm{V}$$
27	20 26	ixpconst	$$⊢\underset{x\in \mathrm{dom}r}{⨉}\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r={\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r}^{\mathrm{dom}r}$$
28	18 27	sseqtri	$$⊢\underset{x\in \mathrm{dom}r}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\right)\subseteq {\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r}^{\mathrm{dom}r}$$
29	2 28	elpwi2	$$⊢\underset{x\in \mathrm{dom}r}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\right)\in 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r}^{\mathrm{dom}r}\right)$$
30	29	rgen2w	$$⊢\forall f\in v\forall g\in v\underset{x\in \mathrm{dom}r}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\right)\in 𝒫\left({\bigcup \mathrm{ran}\bigcup \mathrm{ran}\bigcup \mathrm{ran}r}^{\mathrm{dom}r}\right)$$
31	1 1 3 30	mpoexw	$$⊢\left(f\in v,g\in v⟼\underset{x\in \mathrm{dom}r}{⨉}\left(f\left(x\right)\mathrm{Hom}\left(r\left(x\right)\right)g\left(x\right)\right)\right)\in \mathrm{V}$$