Description: Lemma for frege129 . Proposition 128 of Frege1879 p. 83. (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 | frege128 | |- ( ( M ( ( t+ ` R ) u. _I ) Y -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) -> ( Fun `' `' R -> ( ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) -> ( Y R X -> ( -. 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 | 1 2 3 4 | frege127 | |- ( Fun `' `' R -> ( Y ( t+ ` R ) M -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) |
6 | frege51 | |- ( ( Fun `' `' R -> ( Y ( t+ ` R ) M -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) -> ( ( M ( ( t+ ` R ) u. _I ) Y -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) -> ( Fun `' `' R -> ( ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) ) ) |
|
7 | 5 6 | ax-mp | |- ( ( M ( ( t+ ` R ) u. _I ) Y -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) -> ( Fun `' `' R -> ( ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) -> ( Y R X -> ( -. X ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) X ) ) ) ) ) |