Metamath Proof Explorer


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 V n N r × ˙ n
Assertion ov2ssiunov2 R U N V M N R × ˙ M C R

Proof

Step Hyp Ref Expression
1 ov2ssiunov2.def C = r V n N r × ˙ n
2 simp3 R U N V M N M N
3 simpr R U N V M N n = M n = M
4 3 oveq2d R U N V M N n = M R × ˙ n = R × ˙ M
5 4 eleq2d R U N V M N n = M x R × ˙ n x R × ˙ M
6 2 5 rspcedv R U N V M N x R × ˙ M n N x R × ˙ n
7 1 eliunov2 R U N V x C R n N x R × ˙ n
8 7 biimprd R U N V n N x R × ˙ n x C R
9 8 3adant3 R U N V M N n N x R × ˙ n x C R
10 6 9 syld R U N V M N x R × ˙ M x C R
11 10 ssrdv R U N V M N R × ˙ M C R