Metamath Proof Explorer


Theorem frege108

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

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

Proof

Step Hyp Ref Expression
1 frege108.z
 |-  Z e. A
2 frege108.y
 |-  Y e. B
3 frege108.v
 |-  V e. C
4 frege108.r
 |-  R e. D
5 1 2 3 4 frege102
 |-  ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( t+ ` R ) V ) )
6 3 frege107
 |-  ( ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( t+ ` R ) V ) ) -> ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( ( t+ ` R ) u. _I ) V ) ) )
7 5 6 ax-mp
 |-  ( Z ( ( t+ ` R ) u. _I ) Y -> ( Y R V -> Z ( ( t+ ` R ) u. _I ) V ) )