Metamath Proof Explorer


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 φRV
frege111d.a φAV
frege111d.b φBV
frege111d.c φCV
frege111d.ac φAt+RCA=C
frege111d.cb φCRB
Assertion frege111d φAt+RBA=BBt+RA

Proof

Step Hyp Ref Expression
1 frege111d.r φRV
2 frege111d.a φAV
3 frege111d.b φBV
4 frege111d.c φCV
5 frege111d.ac φAt+RCA=C
6 frege111d.cb φCRB
7 1 2 3 4 5 6 frege108d φAt+RBA=B
8 7 frege114d φAt+RBA=BBt+RA