Theorem frege111d

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

	Ref	Expression
Hypotheses	frege111d.r	$$⊢\phi \to R\in \mathrm{V}$$
	frege111d.a	$$⊢\phi \to A\in \mathrm{V}$$
	frege111d.b	$$⊢\phi \to B\in \mathrm{V}$$
	frege111d.c	$$⊢\phi \to C\in \mathrm{V}$$
	frege111d.ac	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)C\vee A=C\right)$$
	frege111d.cb	$$⊢\phi \to CRB$$
Assertion	frege111d	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)B\vee A=B\vee B\mathrm{t+}\left(R\right)A\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege111d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege111d.a	$$⊢\phi \to A\in \mathrm{V}$$
3		frege111d.b	$$⊢\phi \to B\in \mathrm{V}$$
4		frege111d.c	$$⊢\phi \to C\in \mathrm{V}$$
5		frege111d.ac	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)C\vee A=C\right)$$
6		frege111d.cb	$$⊢\phi \to CRB$$
7	1 2 3 4 5 6	frege108d	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)B\vee A=B\right)$$
8	7	frege114d	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)B\vee A=B\vee B\mathrm{t+}\left(R\right)A\right)$$