Metamath Proof Explorer


Theorem frege122

Description: If X is a result of an application of the single-valued procedure R to Y , then every result of an application of the procedure R to Y belongs to the R -sequence beginning with X . Proposition 122 of Frege1879 p. 79. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege116.x 𝑋𝑈
frege118.y 𝑌𝑉
frege120.a 𝐴𝑊
Assertion frege122 ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 frege116.x 𝑋𝑈
2 frege118.y 𝑌𝑉
3 frege120.a 𝐴𝑊
4 3 frege112 ( 𝐴 = 𝑋𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝐴 )
5 1 2 3 frege121 ( ( 𝐴 = 𝑋𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝐴 ) → ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝐴 ) ) ) )
6 4 5 ax-mp ( Fun 𝑅 → ( 𝑌 𝑅 𝑋 → ( 𝑌 𝑅 𝐴𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝐴 ) ) )