Theorem frege122d

Description: If F is a function, A is the successor of X , and B is the successor of X , then A and B are the same (or B follows A in the transitive closure of F ). Similar to Proposition 122 of Frege1879 p. 79. Compare with frege122 . (Contributed by RP, 15-Jul-2020)

	Ref	Expression
Hypotheses	frege122d.a	⊢ ( 𝜑 → 𝐴 = ( 𝐹 ‘ 𝑋 ) )
	frege122d.b	⊢ ( 𝜑 → 𝐵 = ( 𝐹 ‘ 𝑋 ) )
Assertion	frege122d	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		frege122d.a	⊢ ( 𝜑 → 𝐴 = ( 𝐹 ‘ 𝑋 ) )
2		frege122d.b	⊢ ( 𝜑 → 𝐵 = ( 𝐹 ‘ 𝑋 ) )
3	1 2	eqtr4d	⊢ ( 𝜑 → 𝐴 = 𝐵 )
4	3	olcd	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ) )