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	$$⊢\phi \to R\in \mathrm{V}$$
	frege102d.a	$$⊢\phi \to A\in \mathrm{V}$$
	frege102d.b	$$⊢\phi \to B\in \mathrm{V}$$
	frege102d.c	$$⊢\phi \to C\in \mathrm{V}$$
	frege102d.ac	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)C\vee A=C\right)$$
	frege102d.cb	$$⊢\phi \to CRB$$
Assertion	frege102d	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$

Proof

Step	Hyp	Ref	Expression
1		frege102d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege102d.a	$$⊢\phi \to A\in \mathrm{V}$$
3		frege102d.b	$$⊢\phi \to B\in \mathrm{V}$$
4		frege102d.c	$$⊢\phi \to C\in \mathrm{V}$$
5		frege102d.ac	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)C\vee A=C\right)$$
6		frege102d.cb	$$⊢\phi \to CRB$$
7	1	adantr	$$⊢\left(\phi \wedge A\mathrm{t+}\left(R\right)C\right)\to R\in \mathrm{V}$$
8	2	adantr	$$⊢\left(\phi \wedge A\mathrm{t+}\left(R\right)C\right)\to A\in \mathrm{V}$$
9	3	adantr	$$⊢\left(\phi \wedge A\mathrm{t+}\left(R\right)C\right)\to B\in \mathrm{V}$$
10	4	adantr	$$⊢\left(\phi \wedge A\mathrm{t+}\left(R\right)C\right)\to C\in \mathrm{V}$$
11		simpr	$$⊢\left(\phi \wedge A\mathrm{t+}\left(R\right)C\right)\to A\mathrm{t+}\left(R\right)C$$
12	6	adantr	$$⊢\left(\phi \wedge A\mathrm{t+}\left(R\right)C\right)\to CRB$$
13	7 8 9 10 11 12	frege96d	$$⊢\left(\phi \wedge A\mathrm{t+}\left(R\right)C\right)\to A\mathrm{t+}\left(R\right)B$$
14	1	adantr	$$⊢\left(\phi \wedge A=C\right)\to R\in \mathrm{V}$$
15		simpr	$$⊢\left(\phi \wedge A=C\right)\to A=C$$
16	6	adantr	$$⊢\left(\phi \wedge A=C\right)\to CRB$$
17	15 16	eqbrtrd	$$⊢\left(\phi \wedge A=C\right)\to ARB$$
18	14 17	frege91d	$$⊢\left(\phi \wedge A=C\right)\to A\mathrm{t+}\left(R\right)B$$
19	13 18 5	mpjaodan	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$