Metamath Proof Explorer


Theorem frege126

Description: If M follows Y in the R -sequence and if the procedure R is single-valued, then every result of an application of the procedure R to Y belongs to the R -sequence beginning with M or precedes M in the R -sequence. Proposition 126 of Frege1879 p. 81. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

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

Proof

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