Metamath Proof Explorer


Theorem frege128

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 ) ) ) ) )

Proof

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 ) ) ) ) )