Metamath Proof Explorer


Theorem frege124

Description: If X is a result of an application of the single-valued procedure R to Y and if M follows Y in the R -sequence, then M belongs to the R -sequence beginning with X . Proposition 124 of Frege1879 p. 80. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege123.x 𝑋𝑈
frege123.y 𝑌𝑉
frege124.m 𝑀𝑊
frege124.r 𝑅𝑆
Assertion frege124 ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 frege123.x 𝑋𝑈
2 frege123.y 𝑌𝑉
3 frege124.m 𝑀𝑊
4 frege124.r 𝑅𝑆
5 1 2 3 4 frege110 ( ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) )
6 1 2 frege123 ( ( ∀ 𝑎 ( 𝑌 𝑅 𝑎𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑎 ) → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) ) ) )
7 5 6 ax-mp ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 ( t+ ‘ 𝑅 ) 𝑀𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑀 ) ) )