Metamath Proof Explorer


Theorem frege102

Description: If Z belongs to the R -sequence beginning with X , then every result of an application of the procedure R to Z follows X in the R -sequence. Proposition 102 of Frege1879 p. 72. (Contributed by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege102.x
|- X e. A
frege102.z
|- Z e. B
frege102.v
|- V e. C
frege102.r
|- R e. D
Assertion frege102
|- ( X ( ( t+ ` R ) u. _I ) Z -> ( Z R V -> X ( t+ ` R ) V ) )

Proof

Step Hyp Ref Expression
1 frege102.x
 |-  X e. A
2 frege102.z
 |-  Z e. B
3 frege102.v
 |-  V e. C
4 frege102.r
 |-  R e. D
5 2 3 4 frege92
 |-  ( Z = X -> ( Z R V -> X ( t+ ` R ) V ) )
6 1 2 3 4 frege96
 |-  ( X ( t+ ` R ) Z -> ( Z R V -> X ( t+ ` R ) V ) )
7 2 frege101
 |-  ( ( Z = X -> ( Z R V -> X ( t+ ` R ) V ) ) -> ( ( X ( t+ ` R ) Z -> ( Z R V -> X ( t+ ` R ) V ) ) -> ( X ( ( t+ ` R ) u. _I ) Z -> ( Z R V -> X ( t+ ` R ) V ) ) ) )
8 5 6 7 mp2
 |-  ( X ( ( t+ ` R ) u. _I ) Z -> ( Z R V -> X ( t+ ` R ) V ) )