Metamath Proof Explorer

Theorem frege123

Description: Lemma for frege124 . Proposition 123 of Frege1879 p. 79. (Contributed by RP, 8-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege123.x 
|- X e. U
frege123.y 
|- Y e. V
Assertion frege123 
|- ( ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) ) )

Proof

Step Hyp Ref Expression
1 frege123.x 
 |-  X e. U
2 frege123.y 
 |-  Y e. V
3 vex 
 |-  a e. _V
4 1 2 3 frege122 
 |-  ( Fun `' `' R -> ( Y R X -> ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) ) )
5 4 alrimdv 
 |-  ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) ) )
6 frege19 
 |-  ( ( Fun `' `' R -> ( Y R X -> A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) ) ) -> ( ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) ) ) )
7 5 6 ax-mp 
 |-  ( ( A. a ( Y R a -> X ( ( t+ ` R ) u. _I ) a ) -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) -> ( Fun `' `' R -> ( Y R X -> ( Y ( t+ ` R ) M -> X ( ( t+ ` R ) u. _I ) M ) ) ) )