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 \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n))$
	Assertion	ov2ssiunov2	$⊢ (R \in U \land N \in V \land M \in N) \to R \underset{˙}{\times} M \subseteq C (R)$

Proof

Step	Hyp	Ref	Expression
1		ov2ssiunov2.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n))$
2		simp3	$⊢ (R \in U \land N \in V \land M \in N) \to M \in N$
3		simpr	$⊢ ((R \in U \land N \in V \land M \in N) \land n = M) \to n = M$
4	3	oveq2d	$⊢ ((R \in U \land N \in V \land M \in N) \land n = M) \to R \underset{˙}{\times} n = R \underset{˙}{\times} M$
5	4	eleq2d	$⊢ ((R \in U \land N \in V \land M \in N) \land n = M) \to (x \in (R \underset{˙}{\times} n) \leftrightarrow x \in (R \underset{˙}{\times} M))$
6	2 5	rspcedv	$⊢ (R \in U \land N \in V \land M \in N) \to (x \in (R \underset{˙}{\times} M) \to \exists n \in N x \in (R \underset{˙}{\times} n))$
7	1	eliunov2	$⊢ (R \in U \land N \in V) \to (x \in C (R) \leftrightarrow \exists n \in N x \in (R \underset{˙}{\times} n))$
8	7	biimprd	$⊢ (R \in U \land N \in V) \to (\exists n \in N x \in (R \underset{˙}{\times} n) \to x \in C (R))$
9	8	3adant3	$⊢ (R \in U \land N \in V \land M \in N) \to (\exists n \in N x \in (R \underset{˙}{\times} n) \to x \in C (R))$
10	6 9	syld	$⊢ (R \in U \land N \in V \land M \in N) \to (x \in (R \underset{˙}{\times} M) \to x \in C (R))$
11	10	ssrdv	$⊢ (R \in U \land N \in V \land M \in N) \to R \underset{˙}{\times} M \subseteq C (R)$