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	⊢ ( 𝜑 → 𝑅 ∈ V )
	frege96d.a	⊢ ( 𝜑 → 𝐴 ∈ V )
	frege96d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
	frege96d.c	⊢ ( 𝜑 → 𝐶 ∈ V )
	frege96d.ac	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐶 )
	frege96d.cb	⊢ ( 𝜑 → 𝐶 𝑅 𝐵 )
Assertion	frege96d	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		frege96d.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		frege96d.a	⊢ ( 𝜑 → 𝐴 ∈ V )
3		frege96d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
4		frege96d.c	⊢ ( 𝜑 → 𝐶 ∈ V )
5		frege96d.ac	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐶 )
6		frege96d.cb	⊢ ( 𝜑 → 𝐶 𝑅 𝐵 )
7		brcogw	⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ∧ 𝐶 𝑅 𝐵 ) ) → 𝐴 ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) 𝐵 )
8	2 3 4 5 6 7	syl32anc	⊢ ( 𝜑 → 𝐴 ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) 𝐵 )
9		trclfvlb	⊢ ( 𝑅 ∈ V → 𝑅 ⊆ ( t+ ‘ 𝑅 ) )
10		coss1	⊢ ( 𝑅 ⊆ ( t+ ‘ 𝑅 ) → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) )
11	1 9 10	3syl	⊢ ( 𝜑 → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) )
12		trclfvcotrg	⊢ ( ( t+ ‘ 𝑅 ) ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 )
13	11 12	sstrdi	⊢ ( 𝜑 → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ⊆ ( t+ ‘ 𝑅 ) )
14	13	ssbrd	⊢ ( 𝜑 → ( 𝐴 ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) 𝐵 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ) )
15	8 14	mpd	⊢ ( 𝜑 → 𝐴 ( t+ ‘ 𝑅 ) 𝐵 )