Description: If B follows A in R then B follows A in the transitive closure of R . Similar to Proposition 91 of Frege1879 p. 68. Comparw with frege91 . (Contributed by RP, 15-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | frege91d.r | |- ( ph -> R e. _V ) |
|
| frege91d.ac | |- ( ph -> A R B ) |
||
| Assertion | frege91d | |- ( ph -> A ( t+ ` R ) B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frege91d.r | |- ( ph -> R e. _V ) |
|
| 2 | frege91d.ac | |- ( ph -> A R B ) |
|
| 3 | trclfvlb | |- ( R e. _V -> R C_ ( t+ ` R ) ) |
|
| 4 | 1 3 | syl | |- ( ph -> R C_ ( t+ ` R ) ) |
| 5 | 4 | ssbrd | |- ( ph -> ( A R B -> A ( t+ ` R ) B ) ) |
| 6 | 2 5 | mpd | |- ( ph -> A ( t+ ` R ) B ) |