Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Member of sequence
frege102
Metamath Proof Explorer
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+ ‘ 𝑅 ) 𝑉 ) )