Theorem frege126d

Description: If F is a function, A is the successor of X , and B follows X in the transitive closure of F , then (for distinct A and B ) either A follows B or B follows A in the transitive closure of F . Similar to Proposition 126 of Frege1879 p. 81. Compare with frege126 . (Contributed by RP, 16-Jul-2020)

	Ref	Expression
Hypotheses	frege126d.f	⊢ ( 𝜑 → 𝐹 ∈ V )
	frege126d.x	⊢ ( 𝜑 → 𝑋 ∈ dom 𝐹 )
	frege126d.a	⊢ ( 𝜑 → 𝐴 = ( 𝐹 ‘ 𝑋 ) )
	frege126d.xb	⊢ ( 𝜑 → 𝑋 ( t+ ‘ 𝐹 ) 𝐵 )
	frege126d.fun	⊢ ( 𝜑 → Fun 𝐹 )
Assertion	frege126d	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		frege126d.f	⊢ ( 𝜑 → 𝐹 ∈ V )
2		frege126d.x	⊢ ( 𝜑 → 𝑋 ∈ dom 𝐹 )
3		frege126d.a	⊢ ( 𝜑 → 𝐴 = ( 𝐹 ‘ 𝑋 ) )
4		frege126d.xb	⊢ ( 𝜑 → 𝑋 ( t+ ‘ 𝐹 ) 𝐵 )
5		frege126d.fun	⊢ ( 𝜑 → Fun 𝐹 )
6	1 2 3 4 5	frege124d	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ) )
7	6	frege114d	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝐹 ) 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ( t+ ‘ 𝐹 ) 𝐴 ) )