Metamath Proof Explorer


Theorem frege102

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

Ref Expression
Hypotheses frege102.x 𝑋𝐴
frege102.z 𝑍𝐵
frege102.v 𝑉𝐶
frege102.r 𝑅𝐷
Assertion frege102 ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( 𝑍 𝑅 𝑉𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) )

Proof

Step Hyp Ref Expression
1 frege102.x 𝑋𝐴
2 frege102.z 𝑍𝐵
3 frege102.v 𝑉𝐶
4 frege102.r 𝑅𝐷
5 2 3 4 frege92 ( 𝑍 = 𝑋 → ( 𝑍 𝑅 𝑉𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) )
6 1 2 3 4 frege96 ( 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → ( 𝑍 𝑅 𝑉𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) )
7 2 frege101 ( ( 𝑍 = 𝑋 → ( 𝑍 𝑅 𝑉𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) → ( ( 𝑋 ( t+ ‘ 𝑅 ) 𝑍 → ( 𝑍 𝑅 𝑉𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) → ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( 𝑍 𝑅 𝑉𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) ) ) )
8 5 6 7 mp2 ( 𝑋 ( ( t+ ‘ 𝑅 ) ∪ I ) 𝑍 → ( 𝑍 𝑅 𝑉𝑋 ( t+ ‘ 𝑅 ) 𝑉 ) )