Metamath Proof Explorer


Theorem frege87

Description: If Z is a result of an application of the procedure R to an object Y that follows X in the R -sequence and if every result of an application of the procedure R to X has a property A that is hereditary in the R -sequence, then Z has property A . Proposition 87 of Frege1879 p. 66. (Contributed by RP, 1-Jul-2020) (Revised by RP, 7-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege87.x X U
frege87.y Y V
frege87.z Z W
frege87.r R S
frege87.a A B
Assertion frege87 X t+ R Y w X R w w A R hereditary A Y R Z Z A

Proof

Step Hyp Ref Expression
1 frege87.x X U
2 frege87.y Y V
3 frege87.z Z W
4 frege87.r R S
5 frege87.a A B
6 2 3 frege73 R hereditary A Y A R hereditary A Y R Z Z A
7 1 2 4 5 frege86 R hereditary A Y A R hereditary A Y R Z Z A X t+ R Y w X R w w A R hereditary A Y R Z Z A
8 6 7 ax-mp X t+ R Y w X R w w A R hereditary A Y R Z Z A