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. The index set N is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eliunov2uz.def | |- C = ( r e. _V |-> U_ n e. N ( r .^ n ) ) |
|
| Assertion | eliunov2uz | |- ( ( R e. U /\ N = ( ZZ>= ` M ) ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eliunov2uz.def | |- C = ( r e. _V |-> U_ n e. N ( r .^ n ) ) |
|
| 2 | simpr | |- ( ( R e. U /\ N = ( ZZ>= ` M ) ) -> N = ( ZZ>= ` M ) ) |
|
| 3 | fvex | |- ( ZZ>= ` M ) e. _V |
|
| 4 | 2 3 | eqeltrdi | |- ( ( R e. U /\ N = ( ZZ>= ` M ) ) -> N e. _V ) |
| 5 | 1 | eliunov2 | |- ( ( R e. U /\ N e. _V ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) |
| 6 | 4 5 | syldan | |- ( ( R e. U /\ N = ( ZZ>= ` M ) ) -> ( X e. ( C ` R ) <-> E. n e. N X e. ( R .^ n ) ) ) |