Theorem frege108d

Description: If either A and C are the same or C follows A in the transitive closure of Rand B is the successor to C , then either A and B are the same or B follows A in the transitive closure of R . Similar to Proposition 108 of Frege1879 p. 74. Compare with frege108 . (Contributed by RP, 15-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		frege108d.r	|- ( ph -> R e. _V )
2		frege108d.a	|- ( ph -> A e. _V )
3		frege108d.b	|- ( ph -> B e. _V )
4		frege108d.c	|- ( ph -> C e. _V )
5		frege108d.ac	|- ( ph -> ( A ( t+ ` R ) C \/ A = C ) )
6		frege108d.cb	|- ( ph -> C R B )
7	1 2 3 4 5 6	frege102d	|- ( ph -> A ( t+ ` R ) B )
8	7	frege106d	|- ( ph -> ( A ( t+ ` R ) B \/ A = B ) )