Metamath Proof Explorer

Theorem frege133

Description: If the procedure R is single-valued and if M and Y follow X in the R -sequence, then Y belongs to the R -sequence beginning with M or precedes M in the R -sequence. Proposition 133 of Frege1879 p. 86. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege133.x 
|- X e. U
frege133.y 
|- Y e. V
frege133.m 
|- M e. W
frege133.r 
|- R e. S
Assertion frege133 
|- ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) )

Proof

Step Hyp Ref Expression
1 frege133.x 
 |-  X e. U
2 frege133.y 
 |-  Y e. V
3 frege133.m 
 |-  M e. W
4 frege133.r 
 |-  R e. S
5 fvex 
 |-  ( t+ ` R ) e. _V
6 5 cnvex 
 |-  `' ( t+ ` R ) e. _V
7 imaexg 
 |-  ( `' ( t+ ` R ) e. _V -> ( `' ( t+ ` R ) " { M } ) e. _V )
8 6 7 ax-mp 
 |-  ( `' ( t+ ` R ) " { M } ) e. _V
9 imaundir 
 |-  ( ( ( t+ ` R ) u. _I ) " { M } ) = ( ( ( t+ ` R ) " { M } ) u. ( _I " { M } ) )
10 imaexg 
 |-  ( ( t+ ` R ) e. _V -> ( ( t+ ` R ) " { M } ) e. _V )
11 5 10 ax-mp 
 |-  ( ( t+ ` R ) " { M } ) e. _V
12 imai 
 |-  ( _I " { M } ) = { M }
13 snex 
 |-  { M } e. _V
14 12 13 eqeltri 
 |-  ( _I " { M } ) e. _V
15 11 14 unex 
 |-  ( ( ( t+ ` R ) " { M } ) u. ( _I " { M } ) ) e. _V
16 9 15 eqeltri 
 |-  ( ( ( t+ ` R ) u. _I ) " { M } ) e. _V
17 1 2 4 8 16 frege83 
 |-  ( R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> ( X e. ( `' ( t+ ` R ) " { M } ) -> ( X ( t+ ` R ) Y -> Y e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) )
18 3 elexi 
 |-  M e. _V
19 1 elexi 
 |-  X e. _V
20 18 19 elimasn 
 |-  ( X e. ( `' ( t+ ` R ) " { M } ) <-> <. M , X >. e. `' ( t+ ` R ) )
21 df-br 
 |-  ( M `' ( t+ ` R ) X <-> <. M , X >. e. `' ( t+ ` R ) )
22 18 19 brcnv 
 |-  ( M `' ( t+ ` R ) X <-> X ( t+ ` R ) M )
23 20 21 22 3bitr2i 
 |-  ( X e. ( `' ( t+ ` R ) " { M } ) <-> X ( t+ ` R ) M )
24 elun 
 |-  ( Y e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( Y e. ( `' ( t+ ` R ) " { M } ) \/ Y e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
25 df-or 
 |-  ( ( Y e. ( `' ( t+ ` R ) " { M } ) \/ Y e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. Y e. ( `' ( t+ ` R ) " { M } ) -> Y e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) )
26 2 elexi 
 |-  Y e. _V
27 18 26 elimasn 
 |-  ( Y e. ( `' ( t+ ` R ) " { M } ) <-> <. M , Y >. e. `' ( t+ ` R ) )
28 df-br 
 |-  ( M `' ( t+ ` R ) Y <-> <. M , Y >. e. `' ( t+ ` R ) )
29 18 26 brcnv 
 |-  ( M `' ( t+ ` R ) Y <-> Y ( t+ ` R ) M )
30 27 28 29 3bitr2i 
 |-  ( Y e. ( `' ( t+ ` R ) " { M } ) <-> Y ( t+ ` R ) M )
31 30 notbii 
 |-  ( -. Y e. ( `' ( t+ ` R ) " { M } ) <-> -. Y ( t+ ` R ) M )
32 18 26 elimasn 
 |-  ( Y e. ( ( ( t+ ` R ) u. _I ) " { M } ) <-> <. M , Y >. e. ( ( t+ ` R ) u. _I ) )
33 df-br 
 |-  ( M ( ( t+ ` R ) u. _I ) Y <-> <. M , Y >. e. ( ( t+ ` R ) u. _I ) )
34 32 33 bitr4i 
 |-  ( Y e. ( ( ( t+ ` R ) u. _I ) " { M } ) <-> M ( ( t+ ` R ) u. _I ) Y )
35 31 34 imbi12i 
 |-  ( ( -. Y e. ( `' ( t+ ` R ) " { M } ) -> Y e. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) )
36 24 25 35 3bitri 
 |-  ( Y e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) <-> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) )
37 36 imbi2i 
 |-  ( ( X ( t+ ` R ) Y -> Y e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) <-> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) )
38 23 37 imbi12i 
 |-  ( ( X e. ( `' ( t+ ` R ) " { M } ) -> ( X ( t+ ` R ) Y -> Y e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) <-> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) )
39 38 imbi2i 
 |-  ( ( R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> ( X e. ( `' ( t+ ` R ) " { M } ) -> ( X ( t+ ` R ) Y -> Y e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) ) <-> ( R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) )
40 3 4 frege132 
 |-  ( ( R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) -> ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) )
41 39 40 sylbi 
 |-  ( ( R hereditary ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) -> ( X e. ( `' ( t+ ` R ) " { M } ) -> ( X ( t+ ` R ) Y -> Y e. ( ( `' ( t+ ` R ) " { M } ) u. ( ( ( t+ ` R ) u. _I ) " { M } ) ) ) ) ) -> ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) ) )
42 17 41 ax-mp 
 |-  ( Fun `' `' R -> ( X ( t+ ` R ) M -> ( X ( t+ ` R ) Y -> ( -. Y ( t+ ` R ) M -> M ( ( t+ ` R ) u. _I ) Y ) ) ) )