Metamath Proof Explorer

Theorem frege77

Description: If Y follows X in the R -sequence, if property A is hereditary in the R -sequence, and if every result of an application of the procedure R to X has the property A , then Y has property A . Proposition 77 of Frege1879 p. 62. (Contributed by RP, 29-Jun-2020) (Revised by RP, 2-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege77.x 
|- X e. U
frege77.y 
|- Y e. V
frege77.r 
|- R e. W
frege77.a 
|- A e. B
Assertion frege77 
|- ( X ( t+ ` R ) Y -> ( R hereditary A -> ( A. a ( X R a -> a e. A ) -> Y e. A ) ) )

Proof

Step Hyp Ref Expression
1 frege77.x 
 |-  X e. U
2 frege77.y 
 |-  Y e. V
3 frege77.r 
 |-  R e. W
4 frege77.a 
 |-  A e. B
5 1 2 3 dffrege76 
 |-  ( A. f ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) <-> X ( t+ ` R ) Y )
6 4 frege68c 
 |-  ( ( A. f ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) <-> X ( t+ ` R ) Y ) -> ( X ( t+ ` R ) Y -> [. A / f ]. ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) ) )
7 sbcimg 
 |-  ( A e. B -> ( [. A / f ]. ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) <-> ( [. A / f ]. R hereditary f -> [. A / f ]. ( A. a ( X R a -> a e. f ) -> Y e. f ) ) ) )
8 4 7 ax-mp 
 |-  ( [. A / f ]. ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) <-> ( [. A / f ]. R hereditary f -> [. A / f ]. ( A. a ( X R a -> a e. f ) -> Y e. f ) ) )
9 sbcheg 
 |-  ( A e. B -> ( [. A / f ]. R hereditary f <-> [_ A / f ]_ R hereditary [_ A / f ]_ f ) )
10 4 9 ax-mp 
 |-  ( [. A / f ]. R hereditary f <-> [_ A / f ]_ R hereditary [_ A / f ]_ f )
11 csbconstg 
 |-  ( A e. B -> [_ A / f ]_ R = R )
12 4 11 ax-mp 
 |-  [_ A / f ]_ R = R
13 csbvarg 
 |-  ( A e. B -> [_ A / f ]_ f = A )
14 4 13 ax-mp 
 |-  [_ A / f ]_ f = A
15 heeq12 
 |-  ( ( [_ A / f ]_ R = R /\ [_ A / f ]_ f = A ) -> ( [_ A / f ]_ R hereditary [_ A / f ]_ f <-> R hereditary A ) )
16 12 14 15 mp2an 
 |-  ( [_ A / f ]_ R hereditary [_ A / f ]_ f <-> R hereditary A )
17 10 16 bitri 
 |-  ( [. A / f ]. R hereditary f <-> R hereditary A )
18 sbcimg 
 |-  ( A e. B -> ( [. A / f ]. ( A. a ( X R a -> a e. f ) -> Y e. f ) <-> ( [. A / f ]. A. a ( X R a -> a e. f ) -> [. A / f ]. Y e. f ) ) )
19 4 18 ax-mp 
 |-  ( [. A / f ]. ( A. a ( X R a -> a e. f ) -> Y e. f ) <-> ( [. A / f ]. A. a ( X R a -> a e. f ) -> [. A / f ]. Y e. f ) )
20 sbcal 
 |-  ( [. A / f ]. A. a ( X R a -> a e. f ) <-> A. a [. A / f ]. ( X R a -> a e. f ) )
21 sbcimg 
 |-  ( A e. B -> ( [. A / f ]. ( X R a -> a e. f ) <-> ( [. A / f ]. X R a -> [. A / f ]. a e. f ) ) )
22 4 21 ax-mp 
 |-  ( [. A / f ]. ( X R a -> a e. f ) <-> ( [. A / f ]. X R a -> [. A / f ]. a e. f ) )
23 sbcg 
 |-  ( A e. B -> ( [. A / f ]. X R a <-> X R a ) )
24 4 23 ax-mp 
 |-  ( [. A / f ]. X R a <-> X R a )
25 sbcel2gv 
 |-  ( A e. B -> ( [. A / f ]. a e. f <-> a e. A ) )
26 4 25 ax-mp 
 |-  ( [. A / f ]. a e. f <-> a e. A )
27 24 26 imbi12i 
 |-  ( ( [. A / f ]. X R a -> [. A / f ]. a e. f ) <-> ( X R a -> a e. A ) )
28 22 27 bitri 
 |-  ( [. A / f ]. ( X R a -> a e. f ) <-> ( X R a -> a e. A ) )
29 28 albii 
 |-  ( A. a [. A / f ]. ( X R a -> a e. f ) <-> A. a ( X R a -> a e. A ) )
30 20 29 bitri 
 |-  ( [. A / f ]. A. a ( X R a -> a e. f ) <-> A. a ( X R a -> a e. A ) )
31 sbcel2gv 
 |-  ( A e. B -> ( [. A / f ]. Y e. f <-> Y e. A ) )
32 4 31 ax-mp 
 |-  ( [. A / f ]. Y e. f <-> Y e. A )
33 30 32 imbi12i 
 |-  ( ( [. A / f ]. A. a ( X R a -> a e. f ) -> [. A / f ]. Y e. f ) <-> ( A. a ( X R a -> a e. A ) -> Y e. A ) )
34 19 33 bitri 
 |-  ( [. A / f ]. ( A. a ( X R a -> a e. f ) -> Y e. f ) <-> ( A. a ( X R a -> a e. A ) -> Y e. A ) )
35 17 34 imbi12i 
 |-  ( ( [. A / f ]. R hereditary f -> [. A / f ]. ( A. a ( X R a -> a e. f ) -> Y e. f ) ) <-> ( R hereditary A -> ( A. a ( X R a -> a e. A ) -> Y e. A ) ) )
36 8 35 bitri 
 |-  ( [. A / f ]. ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) <-> ( R hereditary A -> ( A. a ( X R a -> a e. A ) -> Y e. A ) ) )
37 6 36 syl6ib 
 |-  ( ( A. f ( R hereditary f -> ( A. a ( X R a -> a e. f ) -> Y e. f ) ) <-> X ( t+ ` R ) Y ) -> ( X ( t+ ` R ) Y -> ( R hereditary A -> ( A. a ( X R a -> a e. A ) -> Y e. A ) ) ) )
38 5 37 ax-mp 
 |-  ( X ( t+ ` R ) Y -> ( R hereditary A -> ( A. a ( X R a -> a e. A ) -> Y e. A ) ) )