Metamath Proof Explorer

Theorem frege131

Description: If the procedure R is single-valued, then the property of belonging to the R -sequence begining with M or preceeding M in the R -sequence is hereditary in the R -sequence. Proposition 131 of Frege1879 p. 85. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege130.m 
|- M e. U
frege130.r 
|- R e. V
Assertion frege131 
|- ( 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 frege75 
 |-  ( A. b ( b e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> A. a ( b R a -> a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
4 elun 
 |-  ( b e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( b e. ( `' ( t+ ` R ) " { M } ) \/ b e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
5 df-or 
 |-  ( ( b e. ( `' ( t+ ` R ) " { M } ) \/ b e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. b e. ( `' ( t+ ` R ) " { M } ) -> b e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
6 1 elexi 
 |-  M e. _V
7 vex 
 |-  b e. _V
8 6 7 elimasn 
 |-  ( b e. ( `' ( t+ ` R ) " { M } ) <-> <. M , b >. e. `' ( t+ ` R ) )
9 df-br 
 |-  ( M `' ( t+ ` R ) b <-> <. M , b >. e. `' ( t+ ` R ) )
10 6 7 brcnv 
 |-  ( M `' ( t+ ` R ) b <-> b ( t+ ` R ) M )
11 8 9 10 3bitr2i 
 |-  ( b e. ( `' ( t+ ` R ) " { M } ) <-> b ( t+ ` R ) M )
12 11 notbii 
 |-  ( -. b e. ( `' ( t+ ` R ) " { M } ) <-> -. b ( t+ ` R ) M )
13 6 7 elimasn 
 |-  ( b e. ( ( ( t+ ` R ) u. _I ) " { M } ) <-> <. M , b >. e. ( ( t+ ` R ) u. _I ) )
14 df-br 
 |-  ( M ( ( t+ ` R ) u. _I ) b <-> <. M , b >. e. ( ( t+ ` R ) u. _I ) )
15 13 14 bitr4i 
 |-  ( b e. ( ( ( t+ ` R ) u. _I ) " { M } ) <-> M ( ( t+ ` R ) u. _I ) b )
16 12 15 imbi12i 
 |-  ( ( -. b e. ( `' ( t+ ` R ) " { M } ) -> b e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) )
17 4 5 16 3bitri 
 |-  ( b e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. b ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) b ) )
18 elun 
 |-  ( a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( a e. ( `' ( t+ ` R ) " { M } ) \/ a e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
19 df-or 
 |-  ( ( a e. ( `' ( t+ ` R ) " { M } ) \/ a e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. a e. ( `' ( t+ ` R ) " { M } ) -> a e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
20 vex 
 |-  a e. _V
21 6 20 elimasn 
 |-  ( a e. ( `' ( t+ ` R ) " { M } ) <-> <. M , a >. e. `' ( t+ ` R ) )
22 df-br 
 |-  ( M `' ( t+ ` R ) a <-> <. M , a >. e. `' ( t+ ` R ) )
23 6 20 brcnv 
 |-  ( M `' ( t+ ` R ) a <-> a ( t+ ` R ) M )
24 21 22 23 3bitr2i 
 |-  ( a e. ( `' ( t+ ` R ) " { M } ) <-> a ( t+ ` R ) M )
25 24 notbii 
 |-  ( -. a e. ( `' ( t+ ` R ) " { M } ) <-> -. a ( t+ ` R ) M )
26 6 20 elimasn 
 |-  ( a e. ( ( ( t+ ` R ) u. _I ) " { M } ) <-> <. M , a >. e. ( ( t+ ` R ) u. _I ) )
27 df-br 
 |-  ( M ( ( t+ ` R ) u. _I ) a <-> <. M , a >. e. ( ( t+ ` R ) u. _I ) )
28 26 27 bitr4i 
 |-  ( a e. ( ( ( t+ ` R ) u. _I ) " { M } ) <-> M ( ( t+ ` R ) u. _I ) a )
29 25 28 imbi12i 
 |-  ( ( -. a e. ( `' ( t+ ` R ) " { M } ) -> a e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) )
30 18 19 29 3bitri 
 |-  ( a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) )
31 30 imbi2i 
 |-  ( ( b R a -> a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) <-> ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) )
32 31 albii 
 |-  ( A. a ( b R a -> a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) <-> A. a ( b R a -> ( -. a ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) a ) ) )
33 17 32 imbi12i 
 |-  ( ( b e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> A. a ( b R a -> a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) <-> ( ( -. 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 ) ) ) )
34 33 albii 
 |-  ( A. b ( b e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> A. a ( b R a -> a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) <-> 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 ) ) ) )
35 34 imbi1i 
 |-  ( ( A. b ( b e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> A. a ( b R a -> a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) <-> ( 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 } ) ) ) )
36 1 2 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 } ) ) ) )
37 35 36 sylbi 
 |-  ( ( A. b ( b e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> A. a ( b R a -> a e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) -> ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) )
38 3 37 ax-mp 
 |-  ( Fun `' `' R -> R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )