Theorem ov2ssiunov2

Description: Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020)

	Ref	Expression
Hypothesis	ov2ssiunov2.def	|- C = ( r e. _V |-> U_ n e. N ( r .^ n ) )
Assertion	ov2ssiunov2	|- ( ( R e. U /\ N e. V /\ M e. N ) -> ( R .^ M ) C_ ( C ` R ) )

Proof

Step	Hyp	Ref	Expression
1		ov2ssiunov2.def	|- C = ( r e. _V |-> U_ n e. N ( r .^ n ) )
2		simp3	|- ( ( R e. U /\ N e. V /\ M e. N ) -> M e. N )
3		simpr	|- ( ( ( R e. U /\ N e. V /\ M e. N ) /\ n = M ) -> n = M )
4	3	oveq2d	|- ( ( ( R e. U /\ N e. V /\ M e. N ) /\ n = M ) -> ( R .^ n ) = ( R .^ M ) )
5	4	eleq2d	|- ( ( ( R e. U /\ N e. V /\ M e. N ) /\ n = M ) -> ( x e. ( R .^ n ) <-> x e. ( R .^ M ) ) )
6	2 5	rspcedv	|- ( ( R e. U /\ N e. V /\ M e. N ) -> ( x e. ( R .^ M ) -> E. n e. N x e. ( R .^ n ) ) )
7	1	eliunov2	|- ( ( R e. U /\ N e. V ) -> ( x e. ( C ` R ) <-> E. n e. N x e. ( R .^ n ) ) )
8	7	biimprd	|- ( ( R e. U /\ N e. V ) -> ( E. n e. N x e. ( R .^ n ) -> x e. ( C ` R ) ) )
9	8	3adant3	|- ( ( R e. U /\ N e. V /\ M e. N ) -> ( E. n e. N x e. ( R .^ n ) -> x e. ( C ` R ) ) )
10	6 9	syld	|- ( ( R e. U /\ N e. V /\ M e. N ) -> ( x e. ( R .^ M ) -> x e. ( C ` R ) ) )
11	10	ssrdv	|- ( ( R e. U /\ N e. V /\ M e. N ) -> ( R .^ M ) C_ ( C ` R ) )