Theorem eltrclrec

Description: Membership in the indexed union of relation exponentiation over the natural numbers 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	trclrec.def	|- C = ( r e. _V |-> U_ n e. NN ( r ^r n ) )
Assertion	eltrclrec	|- ( R e. V -> ( X e. ( C ` R ) <-> E. n e. NN X e. ( R ^r n ) ) )

Proof

Step	Hyp	Ref	Expression
1		trclrec.def	|- C = ( r e. _V |-> U_ n e. NN ( r ^r n ) )
2		nnex	|- NN e. _V
3	1	eliunov2	|- ( ( R e. V /\ NN e. _V ) -> ( X e. ( C ` R ) <-> E. n e. NN X e. ( R ^r n ) ) )
4	2 3	mpan2	|- ( R e. V -> ( X e. ( C ` R ) <-> E. n e. NN X e. ( R ^r n ) ) )