Description: Two classes related by the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | brtrclrec.def | |- C = ( r e. _V |-> U_ n e. NN ( r ^r n ) ) |
|
Assertion | brtrclrec | |- ( R e. V -> ( X ( C ` R ) Y <-> E. n e. NN X ( R ^r n ) Y ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brtrclrec.def | |- C = ( r e. _V |-> U_ n e. NN ( r ^r n ) ) |
|
2 | nnex | |- NN e. _V |
|
3 | 1 | briunov2 | |- ( ( R e. V /\ NN e. _V ) -> ( X ( C ` R ) Y <-> E. n e. NN X ( R ^r n ) Y ) ) |
4 | 2 3 | mpan2 | |- ( R e. V -> ( X ( C ` R ) Y <-> E. n e. NN X ( R ^r n ) Y ) ) |