Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter III Single-valued procedures
frege124
Metamath Proof Explorer
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 ) 𝑀 ) ) )