Metamath Proof Explorer


Theorem frege102d

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 B follows A in the transitive closure of R . Similar to Proposition 102 of Frege1879 p. 72. Compare with frege102 . (Contributed by RP, 15-Jul-2020)

Ref Expression
Hypotheses frege102d.r φRV
frege102d.a φAV
frege102d.b φBV
frege102d.c φCV
frege102d.ac φAt+RCA=C
frege102d.cb φCRB
Assertion frege102d φAt+RB

Proof

Step Hyp Ref Expression
1 frege102d.r φRV
2 frege102d.a φAV
3 frege102d.b φBV
4 frege102d.c φCV
5 frege102d.ac φAt+RCA=C
6 frege102d.cb φCRB
7 1 adantr φAt+RCRV
8 2 adantr φAt+RCAV
9 3 adantr φAt+RCBV
10 4 adantr φAt+RCCV
11 simpr φAt+RCAt+RC
12 6 adantr φAt+RCCRB
13 7 8 9 10 11 12 frege96d φAt+RCAt+RB
14 1 adantr φA=CRV
15 simpr φA=CA=C
16 6 adantr φA=CCRB
17 15 16 eqbrtrd φA=CARB
18 14 17 frege91d φA=CAt+RB
19 13 18 5 mpjaodan φAt+RB