Theorem frege91d

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	⊢ ( 𝜑 → 𝑅 ∈ V )
	frege91d.ac	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion	frege91d	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		frege91d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		frege91d.ac	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3		trclfvlb	⊢ ( 𝑅 ∈ V → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
4	1 3	syl	⊢ ( 𝜑 → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
5	4	ssbrd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ) )
6	2 5	mpd	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )