Metamath Proof Explorer


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
|- ( ph -> F e. _V )
frege126d.x
|- ( ph -> X e. dom F )
frege126d.a
|- ( ph -> A = ( F ` X ) )
frege126d.xb
|- ( ph -> X ( t+ ` F ) B )
frege126d.fun
|- ( ph -> Fun F )
Assertion frege126d
|- ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )

Proof

Step Hyp Ref Expression
1 frege126d.f
 |-  ( ph -> F e. _V )
2 frege126d.x
 |-  ( ph -> X e. dom F )
3 frege126d.a
 |-  ( ph -> A = ( F ` X ) )
4 frege126d.xb
 |-  ( ph -> X ( t+ ` F ) B )
5 frege126d.fun
 |-  ( ph -> Fun F )
6 1 2 3 4 5 frege124d
 |-  ( ph -> ( A ( t+ ` F ) B \/ A = B ) )
7 6 frege114d
 |-  ( ph -> ( A ( t+ ` F ) B \/ A = B \/ B ( t+ ` F ) A ) )