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

Proof

Step	Hyp	Ref	Expression
1		frege96d.r	$$⊢\phi \to R\in \mathrm{V}$$
2		frege96d.a	$$⊢\phi \to A\in \mathrm{V}$$
3		frege96d.b	$$⊢\phi \to B\in \mathrm{V}$$
4		frege96d.c	$$⊢\phi \to C\in \mathrm{V}$$
5		frege96d.ac	$$⊢\phi \to A\mathrm{t+}\left(R\right)C$$
6		frege96d.cb	$$⊢\phi \to CRB$$
7		brcogw	$$⊢\left(\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\wedge \left(A\mathrm{t+}\left(R\right)C\wedge CRB\right)\right)\to A\left(R\circ \mathrm{t+}\left(R\right)\right)B$$
8	2 3 4 5 6 7	syl32anc	$$⊢\phi \to A\left(R\circ \mathrm{t+}\left(R\right)\right)B$$
9		trclfvlb	$$⊢R\in \mathrm{V}\to R\subseteq \mathrm{t+}\left(R\right)$$
10		coss1	$$⊢R\subseteq \mathrm{t+}\left(R\right)\to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)$$
11	1 9 10	3syl	$$⊢\phi \to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)$$
12		trclfvcotrg	$$⊢\mathrm{t+}\left(R\right)\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
13	11 12	sstrdi	$$⊢\phi \to R\circ \mathrm{t+}\left(R\right)\subseteq \mathrm{t+}\left(R\right)$$
14	13	ssbrd	$$⊢\phi \to \left(A\left(R\circ \mathrm{t+}\left(R\right)\right)B\to A\mathrm{t+}\left(R\right)B\right)$$
15	8 14	mpd	$$⊢\phi \to A\mathrm{t+}\left(R\right)B$$