Metamath Proof Explorer


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 φ R V
frege96d.a φ A V
frege96d.b φ B V
frege96d.c φ C V
frege96d.ac φ A t+ R C
frege96d.cb φ C R B
Assertion frege96d φ A t+ R B

Proof

Step Hyp Ref Expression
1 frege96d.r φ R V
2 frege96d.a φ A V
3 frege96d.b φ B V
4 frege96d.c φ C V
5 frege96d.ac φ A t+ R C
6 frege96d.cb φ C R B
7 brcogw A V B V C V A t+ R C C R B A R t+ R B
8 2 3 4 5 6 7 syl32anc φ A R t+ R B
9 trclfvlb R V R t+ R
10 coss1 R t+ R R t+ R t+ R t+ R
11 1 9 10 3syl φ R t+ R t+ R t+ R
12 trclfvcotrg t+ R t+ R t+ R
13 11 12 sstrdi φ R t+ R t+ R
14 13 ssbrd φ A R t+ R B A t+ R B
15 8 14 mpd φ A t+ R B