Metamath Proof Explorer

Theorem frege98d

Description: If C follows A and B follows C in the transitive closure of R , then B follows A in the transitive closure of R . Similar to Proposition 98 of Frege1879 p. 71. Compare with frege98 . (Contributed by RP, 15-Jul-2020)

		Ref	Expression
	Hypotheses	frege98d.a	$⊢ φ \to A \in V$
		frege98d.b	$⊢ φ \to B \in V$
		frege98d.c	$⊢ φ \to C \in V$
		frege98d.ac	$⊢ φ \to A t+ (R) C$
		frege98d.cb	$⊢ φ \to C t+ (R) B$
	Assertion	frege98d	$⊢ φ \to A t+ (R) B$

Proof

Step	Hyp	Ref	Expression
1		frege98d.a	$⊢ φ \to A \in V$
2		frege98d.b	$⊢ φ \to B \in V$
3		frege98d.c	$⊢ φ \to C \in V$
4		frege98d.ac	$⊢ φ \to A t+ (R) C$
5		frege98d.cb	$⊢ φ \to C t+ (R) B$
6		brcogw	$⊢ ((A \in V \land B \in V \land C \in V) \land (A t+ (R) C \land C t+ (R) B)) \to A (t+ (R) \circ t+ (R)) B$
7	1 2 3 4 5 6	syl32anc	$⊢ φ \to A (t+ (R) \circ t+ (R)) B$
8		trclfvcotrg	$⊢ t+ (R) \circ t+ (R) \subseteq t+ (R)$
9	8	a1i	$⊢ φ \to t+ (R) \circ t+ (R) \subseteq t+ (R)$
10	9	ssbrd	$⊢ φ \to (A (t+ (R) \circ t+ (R)) B \to A t+ (R) B)$
11	7 10	mpd	$⊢ φ \to A t+ (R) B$