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	$⊢ (f \in v, g \in v ⟼ \underset{x \in dom r}{⨉} (f (x) Hom (r (x)) g (x))) \in V$

Proof

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

Metamath Proof Explorer

Theorem prdsvallem

Proof