Description: If M follows Y in the R -sequence and if the procedure R is single-valued, then every result of an application of the procedure R to Y belongs to the R -sequence beginning with M or precedes M in the R -sequence. Proposition 126 of Frege1879 p. 81. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | frege123.x | |- X e. U |
|
| frege123.y | |- Y e. V |
||
| frege124.m | |- M e. W |
||
| frege124.r | |- R e. S |
||
| Assertion | frege126 | |- ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | frege123.x | |- X e. U |
|
| 2 | frege123.y | |- Y e. V |
|
| 3 | frege124.m | |- M e. W |
|
| 4 | frege124.r | |- R e. S |
|
| 5 | 3 1 | frege114 | |- ( X ( ( t+ ` R ) u. _I ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) |
| 6 | 1 2 3 4 | frege125 | |- ( ( X ( ( t+ ` R ) u. _I ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) ) |
| 7 | 5 6 | ax-mp | |- ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) |