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

Proof

Step Hyp Ref Expression
1 frege102d.r φ R V
2 frege102d.a φ A V
3 frege102d.b φ B V
4 frege102d.c φ C V
5 frege102d.ac φ A t+ R C A = C
6 frege102d.cb φ C R B
7 1 adantr φ A t+ R C R V
8 2 adantr φ A t+ R C A V
9 3 adantr φ A t+ R C B V
10 4 adantr φ A t+ R C C V
11 simpr φ A t+ R C A t+ R C
12 6 adantr φ A t+ R C C R B
13 7 8 9 10 11 12 frege96d φ A t+ R C A t+ R B
14 1 adantr φ A = C R V
15 simpr φ A = C A = C
16 6 adantr φ A = C C R B
17 15 16 eqbrtrd φ A = C A R B
18 14 17 frege91d φ A = C A t+ R B
19 13 18 5 mpjaodan φ A t+ R B