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=rVnNr×˙n
Assertion ov2ssiunov2 RUNVMNR×˙MCR

Proof

Step Hyp Ref Expression
1 ov2ssiunov2.def C=rVnNr×˙n
2 simp3 RUNVMNMN
3 simpr RUNVMNn=Mn=M
4 3 oveq2d RUNVMNn=MR×˙n=R×˙M
5 4 eleq2d RUNVMNn=MxR×˙nxR×˙M
6 2 5 rspcedv RUNVMNxR×˙MnNxR×˙n
7 1 eliunov2 RUNVxCRnNxR×˙n
8 7 biimprd RUNVnNxR×˙nxCR
9 8 3adant3 RUNVMNnNxR×˙nxCR
10 6 9 syld RUNVMNxR×˙MxCR
11 10 ssrdv RUNVMNR×˙MCR