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
⊢ X ∈ U
frege123.y
⊢ Y ∈ V
frege124.m
⊢ M ∈ W
frege124.r
⊢ R ∈ S
Assertion
frege124
⊢ Fun ⁡ R -1 -1 → Y R X → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M
Proof
Step
Hyp
Ref
Expression
1
frege123.x
⊢ X ∈ U
2
frege123.y
⊢ Y ∈ V
3
frege124.m
⊢ M ∈ W
4
frege124.r
⊢ R ∈ S
5
1 2 3 4
frege110
⊢ ∀ a Y R a → X t+ ⁡ R ∪ I a → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M
6
1 2
frege123
⊢ ∀ a Y R a → X t+ ⁡ R ∪ I a → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M → Fun ⁡ R -1 -1 → Y R X → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M
7
5 6
ax-mp
⊢ Fun ⁡ R -1 -1 → Y R X → Y t+ ⁡ R M → X t+ ⁡ R ∪ I M