Description: If two elements are connected by the reflexive-transitive closure of a relation, then they are connected via n instances the relation, for some natural number n . Similar of dfrtrclrec2 . (Contributed by RP, 22-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | brfvrtrcld.r | |- ( ph -> R e. _V ) |
|
| Assertion | brfvrtrcld | |- ( ph -> ( A ( t* ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brfvrtrcld.r | |- ( ph -> R e. _V ) |
|
| 2 | dfrtrcl3 | |- t* = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) |
|
| 3 | ssidd | |- ( ph -> NN0 C_ NN0 ) |
|
| 4 | 2 1 3 | brmptiunrelexpd | |- ( ph -> ( A ( t* ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) ) |