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	⊢ ( 𝜑 → 𝑅 ∈ V )
	frege111d.a	⊢ ( 𝜑 → 𝐴 ∈ V )
	frege111d.b	⊢ ( 𝜑 → 𝐵 ∈ V )
	frege111d.c	⊢ ( 𝜑 → 𝐶 ∈ V )
	frege111d.ac	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐶 ∨ 𝐴 = 𝐶 ) )
	frege111d.cb	⊢ ( 𝜑 → 𝐶 𝑅 𝐵 )
Assertion	frege111d	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝑅 ) 𝐴 ) )

Proof

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