Metamath Proof Explorer


Theorem elrtrclrec

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 ) ) )

Proof

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 ) ) )