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	$$⊢\phi \to F\in \mathrm{V}$$
	frege126d.x	$$⊢\phi \to X\in \mathrm{dom}F$$
	frege126d.a	$$⊢\phi \to A=F\left(X\right)$$
	frege126d.xb	$$⊢\phi \to X\mathrm{t+}\left(F\right)B$$
	frege126d.fun	$$⊢\phi \to \mathrm{Fun}F$$
Assertion	frege126d	$$⊢\phi \to \left(A\mathrm{t+}\left(F\right)B\vee A=B\vee B\mathrm{t+}\left(F\right)A\right)$$

Proof

Step	Hyp	Ref	Expression
1		frege126d.f	$$⊢\phi \to F\in \mathrm{V}$$
2		frege126d.x	$$⊢\phi \to X\in \mathrm{dom}F$$
3		frege126d.a	$$⊢\phi \to A=F\left(X\right)$$
4		frege126d.xb	$$⊢\phi \to X\mathrm{t+}\left(F\right)B$$
5		frege126d.fun	$$⊢\phi \to \mathrm{Fun}F$$
6	1 2 3 4 5	frege124d	$$⊢\phi \to \left(A\mathrm{t+}\left(F\right)B\vee A=B\right)$$
7	6	frege114d	$$⊢\phi \to \left(A\mathrm{t+}\left(F\right)B\vee A=B\vee B\mathrm{t+}\left(F\right)A\right)$$