Metamath Proof Explorer


Theorem frege108d

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

Ref Expression
Hypotheses frege108d.r ( 𝜑𝑅 ∈ V )
frege108d.a ( 𝜑𝐴 ∈ V )
frege108d.b ( 𝜑𝐵 ∈ V )
frege108d.c ( 𝜑𝐶 ∈ V )
frege108d.ac ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐶𝐴 = 𝐶 ) )
frege108d.cb ( 𝜑𝐶 𝑅 𝐵 )
Assertion frege108d ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 frege108d.r ( 𝜑𝑅 ∈ V )
2 frege108d.a ( 𝜑𝐴 ∈ V )
3 frege108d.b ( 𝜑𝐵 ∈ V )
4 frege108d.c ( 𝜑𝐶 ∈ V )
5 frege108d.ac ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐶𝐴 = 𝐶 ) )
6 frege108d.cb ( 𝜑𝐶 𝑅 𝐵 )
7 1 2 3 4 5 6 frege102d ( 𝜑𝐴 ( t+ ‘ 𝑅 ) 𝐵 )
8 7 frege106d ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵𝐴 = 𝐵 ) )