eliunov2

Description: Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the element is a member of that operator value. Generalized from dfrtrclrec2 . (Contributed by RP, 1-Jun-2020)

		Ref	Expression
	Hypothesis	mptiunov2.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n))$
	Assertion	eliunov2	$⊢ (R \in U \land N \in V) \to (X \in C (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))$

Proof

Step	Hyp	Ref	Expression
1		mptiunov2.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n))$
2		eqid	$⊢ (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n))$
3		oveq1	$⊢ r = R \to r \underset{˙}{\times} n = R \underset{˙}{\times} n$
4	3	iuneq2d	$⊢ r = R \to ⋃_{n \in N} (r \underset{˙}{\times} n) = ⋃_{n \in N} (R \underset{˙}{\times} n)$
5		elex	$⊢ R \in U \to R \in V$
6	5	adantr	$⊢ (R \in U \land N \in V) \to R \in V$
7		simpr	$⊢ (R \in U \land N \in V) \to N \in V$
8		ovex	$⊢ R \underset{˙}{\times} n \in V$
9	8	rgenw	$⊢ \forall n \in N R \underset{˙}{\times} n \in V$
10		iunexg	$⊢ (N \in V \land \forall n \in N R \underset{˙}{\times} n \in V) \to ⋃_{n \in N} (R \underset{˙}{\times} n) \in V$
11	7 9 10	sylancl	$⊢ (R \in U \land N \in V) \to ⋃_{n \in N} (R \underset{˙}{\times} n) \in V$
12	2 4 6 11	fvmptd3	$⊢ (R \in U \land N \in V) \to (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) = ⋃_{n \in N} (R \underset{˙}{\times} n)$
13		eleq2	$⊢ (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) = ⋃_{n \in N} (R \underset{˙}{\times} n) \to (X \in (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) \leftrightarrow X \in ⋃_{n \in N} (R \underset{˙}{\times} n))$
14		eliun	$⊢ X \in ⋃_{n \in N} (R \underset{˙}{\times} n) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n)$
15	14	a1i	$⊢ (R \in U \land N \in V) \to (X \in ⋃_{n \in N} (R \underset{˙}{\times} n) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))$
16	13 15	sylan9bb	$⊢ ((r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) = ⋃_{n \in N} (R \underset{˙}{\times} n) \land (R \in U \land N \in V)) \to (X \in (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))$
17	12 16	mpancom	$⊢ (R \in U \land N \in V) \to (X \in (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))$
18		fveq1	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) \to C (R) = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R)$
19	18	eleq2d	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) \to (X \in C (R) \leftrightarrow X \in (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R))$
20	19	bibi1d	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) \to ((X \in C (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n)) \leftrightarrow (X \in (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n)))$
21	20	imbi2d	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) \to (((R \in U \land N \in V) \to (X \in C (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))) \leftrightarrow ((R \in U \land N \in V) \to (X \in (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))))$
22	1 21	ax-mp	$⊢ ((R \in U \land N \in V) \to (X \in C (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))) \leftrightarrow ((R \in U \land N \in V) \to (X \in (r \in V ⟼ ⋃_{n \in N} (r \underset{˙}{\times} n)) (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n)))$
23	17 22	mpbir	$⊢ (R \in U \land N \in V) \to (X \in C (R) \leftrightarrow \exists n \in N X \in (R \underset{˙}{\times} n))$

Metamath Proof Explorer

Theorem eliunov2

Proof