Metamath Proof Explorer

Theorem frege130

Description: Lemma for frege131 . Proposition 130 of Frege1879 p. 84. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege130.m 
|- M e. U
frege130.r 
|- R e. V
Assertion frege130 
|- ( ( A. b ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) -> ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) )

Proof

Step Hyp Ref Expression
1 frege130.m 
 |-  M e. U
2 frege130.r 
 |-  R e. V
3 vex 
 |-  a e. _V
4 vex 
 |-  b e. _V
5 3 4 1 2 frege129 
 |-  ( Fun `' `' R -> ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) )
6 5 alrimdv 
 |-  ( Fun `' `' R -> ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) )
7 6 alrimiv 
 |-  ( Fun `' `' R -> A. b ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) )
8 frege9 
 |-  ( ( Fun `' `' R -> A. b ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) ) -> ( ( A. b ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) -> ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) )
9 7 8 ax-mp 
 |-  ( ( A. b ( ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) -> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) -> ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) )