Theorem frege96d

Description: If C follows A in the transitive closure of R and B follows C in R , then B follows A in the transitive closure of R . Similar to Proposition 96 of Frege1879 p. 71. Compare with frege96 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypotheses	frege96d.r	|- ( ph -> R e. _V )
	frege96d.a	|- ( ph -> A e. _V )
	frege96d.b	|- ( ph -> B e. _V )
	frege96d.c	|- ( ph -> C e. _V )
	frege96d.ac	|- ( ph -> A ( t+ ` R ) C )
	frege96d.cb	|- ( ph -> C R B )
Assertion	frege96d	|- ( ph -> A ( t+ ` R ) B )

Proof

Step	Hyp	Ref	Expression
1		frege96d.r	|- ( ph -> R e. _V )
2		frege96d.a	|- ( ph -> A e. _V )
3		frege96d.b	|- ( ph -> B e. _V )
4		frege96d.c	|- ( ph -> C e. _V )
5		frege96d.ac	|- ( ph -> A ( t+ ` R ) C )
6		frege96d.cb	|- ( ph -> C R B )
7		brcogw	|- ( ( ( A e. _V /\ B e. _V /\ C e. _V ) /\ ( A ( t+ ` R ) C /\ C R B ) ) -> A ( R o. ( t+ ` R ) ) B )
8	2 3 4 5 6 7	syl32anc	|- ( ph -> A ( R o. ( t+ ` R ) ) B )
9		trclfvlb	|- ( R e. _V -> R C_ ( t+ ` R ) )
10		coss1	|- ( R C_ ( t+ ` R ) -> ( R o. ( t+ ` R ) ) C_ ( ( t+ ` R ) o. ( t+ ` R ) ) )
11	1 9 10	3syl	|- ( ph -> ( R o. ( t+ ` R ) ) C_ ( ( t+ ` R ) o. ( t+ ` R ) ) )
12		trclfvcotrg	|- ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R )
13	11 12	sstrdi	|- ( ph -> ( R o. ( t+ ` R ) ) C_ ( t+ ` R ) )
14	13	ssbrd	|- ( ph -> ( A ( R o. ( t+ ` R ) ) B -> A ( t+ ` R ) B ) )
15	8 14	mpd	|- ( ph -> A ( t+ ` R ) B )