Description: Membership in the indexed union of relation exponentiation over the natural numbers (including zero) is equivalent to the existence of at least one number such that the element is a member of that relationship power. (Contributed by RP, 2-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rtrclrec.def | |- C = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) |
|
Assertion | elrtrclrec | |- ( R e. V -> ( X e. ( C ` R ) <-> E. n e. NN0 X e. ( R ^r n ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rtrclrec.def | |- C = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) |
|
2 | nn0ex | |- NN0 e. _V |
|
3 | 1 | eliunov2 | |- ( ( R e. V /\ NN0 e. _V ) -> ( X e. ( C ` R ) <-> E. n e. NN0 X e. ( R ^r n ) ) ) |
4 | 2 3 | mpan2 | |- ( R e. V -> ( X e. ( C ` R ) <-> E. n e. NN0 X e. ( R ^r n ) ) ) |