Description: If two elements are connected by the transitive closure of a relation, then they are connected via n instances the relation, for some counting number n . (Contributed by RP, 22-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | brfvtrcld.r | |- ( ph -> R e. _V ) |
|
| Assertion | brfvtrcld | |- ( ph -> ( A ( t+ ` R ) B <-> E. n e. NN A ( R ^r n ) B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brfvtrcld.r | |- ( ph -> R e. _V ) |
|
| 2 | dftrcl3 | |- t+ = ( r e. _V |-> U_ n e. NN ( r ^r n ) ) |
|
| 3 | nnssnn0 | |- NN C_ NN0 |
|
| 4 | 3 | a1i | |- ( ph -> NN C_ NN0 ) |
| 5 | 2 1 4 | brmptiunrelexpd | |- ( ph -> ( A ( t+ ` R ) B <-> E. n e. NN A ( R ^r n ) B ) ) |