Theorem 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 e. _V |-> U_ n e. N ( r .^ n ) )
Assertion	eliunov2	|- ( ( R e. U /\ N e. V ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) )

Proof

Step	Hyp	Ref	Expression
1		mptiunov2.def	|- C = ( r e. _V |-> U_ n e. N ( r .^ n ) )
2		eqid	|- ( r e. _V |-> U_ n e. N ( r .^ n ) ) = ( r e. _V |-> U_ n e. N ( r .^ n ) )
3		oveq1	|- ( r = R -> ( r .^ n ) = ( R .^ n ) )
4	3	iuneq2d	|- ( r = R -> U_ n e. N ( r .^ n ) = U_ n e. N ( R .^ n ) )
5		elex	|- ( R e. U -> R e. _V )
6	5	adantr	|- ( ( R e. U /\ N e. V ) -> R e. _V )
7		simpr	|- ( ( R e. U /\ N e. V ) -> N e. V )
8		ovex	|- ( R .^ n ) e. _V
9	8	rgenw	|- A. n e. N ( R .^ n ) e. _V
10		iunexg	|- ( ( N e. V /\ A. n e. N ( R .^ n ) e. _V ) -> U_ n e. N ( R .^ n ) e. _V )
11	7 9 10	sylancl	|- ( ( R e. U /\ N e. V ) -> U_ n e. N ( R .^ n ) e. _V )
12	2 4 6 11	fvmptd3	|- ( ( R e. U /\ N e. V ) -> ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) = U_ n e. N ( R .^ n ) )
13		eleq2	|- ( ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) = U_ n e. N ( R .^ n ) -> ( X e. ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) <-> X e. U_ n e. N ( R .^ n ) ) )
14		eliun	|- ( X e. U_ n e. N ( R .^ n ) <-> E. n e. N X e. ( R .^ n ) )
15	14	a1i	|- ( ( R e. U /\ N e. V ) -> ( X e. U_ n e. N ( R .^ n ) <-> E. n e. N X e. ( R .^ n ) ) )
16	13 15	sylan9bb	|- ( ( ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) = U_ n e. N ( R .^ n ) /\ ( R e. U /\ N e. V ) ) -> ( X e. ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) <-> E. n e. N X e. ( R .^ n ) ) )
17	12 16	mpancom	|- ( ( R e. U /\ N e. V ) -> ( X e. ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) <-> E. n e. N X e. ( R .^ n ) ) )
18		fveq1	|- ( C = ( r e. _V |-> U_ n e. N ( r .^ n ) ) -> ( C ` R ) = ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) )
19	18	eleq2d	|- ( C = ( r e. _V |-> U_ n e. N ( r .^ n ) ) -> ( X e. ( C ` R ) <-> X e. ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) ) )
20	19	bibi1d	|- ( C = ( r e. _V |-> U_ n e. N ( r .^ n ) ) -> ( ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) <-> ( X e. ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) )
21	20	imbi2d	|- ( C = ( r e. _V |-> U_ n e. N ( r .^ n ) ) -> ( ( ( R e. U /\ N e. V ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) <-> ( ( R e. U /\ N e. V ) -> ( X e. ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) ) )
22	1 21	ax-mp	|- ( ( ( R e. U /\ N e. V ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) <-> ( ( R e. U /\ N e. V ) -> ( X e. ( ( r e. _V |-> U_ n e. N ( r .^ n ) ) ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) )
23	17 22	mpbir	|- ( ( R e. U /\ N e. V ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) )