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 𝑍𝐴
frege108.y 𝑌𝐵
frege108.v 𝑉𝐶
frege108.r 𝑅𝐷
Assertion frege108 ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 → ( 𝑌 𝑅 𝑉𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑉 ) )

Proof

Step Hyp Ref Expression
1 frege108.z 𝑍𝐴
2 frege108.y 𝑌𝐵
3 frege108.v 𝑉𝐶
4 frege108.r 𝑅𝐷
5 1 2 3 4 frege102 ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 → ( 𝑌 𝑅 𝑉𝑍 ( t+ ‘ 𝑅 ) 𝑉 ) )
6 3 frege107 ( ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 → ( 𝑌 𝑅 𝑉𝑍 ( t+ ‘ 𝑅 ) 𝑉 ) ) → ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 → ( 𝑌 𝑅 𝑉𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑉 ) ) )
7 5 6 ax-mp ( 𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑌 → ( 𝑌 𝑅 𝑉𝑍 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑉 ) )