Metamath Proof Explorer


Theorem frege111

Description: If Y belongs to the R -sequence beginning with Z , then every result of an application of the procedure R to Y belongs to the R -sequence beginning with Z or precedes Z in the R -sequence. Proposition 111 of Frege1879 p. 75. (Contributed by RP, 7-Jul-2020) (Revised by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege111.z Z A
frege111.y Y B
frege111.v V C
frege111.r R D
Assertion frege111 Z t+ R I Y Y R V ¬ V t+ R Z Z t+ R I V

Proof

Step Hyp Ref Expression
1 frege111.z Z A
2 frege111.y Y B
3 frege111.v V C
4 frege111.r R D
5 1 2 3 4 frege108 Z t+ R I Y Y R V Z t+ R I V
6 frege25 Z t+ R I Y Y R V Z t+ R I V Z t+ R I Y Y R V ¬ V t+ R Z Z t+ R I V
7 5 6 ax-mp Z t+ R I Y Y R V ¬ V t+ R Z Z t+ R I V