Theorem frege102d

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 B follows A in the transitive closure of R . Similar to Proposition 102 of Frege1879 p. 72. Compare with frege102 . (Contributed by RP, 15-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		frege102d.r	|- ( ph -> R e. _V )
2		frege102d.a	|- ( ph -> A e. _V )
3		frege102d.b	|- ( ph -> B e. _V )
4		frege102d.c	|- ( ph -> C e. _V )
5		frege102d.ac	|- ( ph -> ( A ( t+ ` R ) C \/ A = C ) )
6		frege102d.cb	|- ( ph -> C R B )
7	1	adantr	|- ( ( ph /\ A ( t+ ` R ) C ) -> R e. _V )
8	2	adantr	|- ( ( ph /\ A ( t+ ` R ) C ) -> A e. _V )
9	3	adantr	|- ( ( ph /\ A ( t+ ` R ) C ) -> B e. _V )
10	4	adantr	|- ( ( ph /\ A ( t+ ` R ) C ) -> C e. _V )
11		simpr	|- ( ( ph /\ A ( t+ ` R ) C ) -> A ( t+ ` R ) C )
12	6	adantr	|- ( ( ph /\ A ( t+ ` R ) C ) -> C R B )
13	7 8 9 10 11 12	frege96d	|- ( ( ph /\ A ( t+ ` R ) C ) -> A ( t+ ` R ) B )
14	1	adantr	|- ( ( ph /\ A = C ) -> R e. _V )
15		simpr	|- ( ( ph /\ A = C ) -> A = C )
16	6	adantr	|- ( ( ph /\ A = C ) -> C R B )
17	15 16	eqbrtrd	|- ( ( ph /\ A = C ) -> A R B )
18	14 17	frege91d	|- ( ( ph /\ A = C ) -> A ( t+ ` R ) B )
19	13 18 5	mpjaodan	|- ( ph -> A ( t+ ` R ) B )