Metamath Proof Explorer


Theorem frege72

Description: If property A is hereditary in the R -sequence, if x has property A , and if y is a result of an application of the procedure R to x , then y has property A . Proposition 72 of Frege1879 p. 59. (Contributed by RP, 28-Mar-2020) (Revised by RP, 5-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypotheses frege72.x
|- X e. U
frege72.y
|- Y e. V
Assertion frege72
|- ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) )

Proof

Step Hyp Ref Expression
1 frege72.x
 |-  X e. U
2 frege72.y
 |-  Y e. V
3 2 frege58c
 |-  ( A. z ( X R z -> z e. A ) -> [. Y / z ]. ( X R z -> z e. A ) )
4 sbcim1
 |-  ( [. Y / z ]. ( X R z -> z e. A ) -> ( [. Y / z ]. X R z -> [. Y / z ]. z e. A ) )
5 sbcbr2g
 |-  ( Y e. V -> ( [. Y / z ]. X R z <-> X R [_ Y / z ]_ z ) )
6 csbvarg
 |-  ( Y e. V -> [_ Y / z ]_ z = Y )
7 6 breq2d
 |-  ( Y e. V -> ( X R [_ Y / z ]_ z <-> X R Y ) )
8 5 7 bitrd
 |-  ( Y e. V -> ( [. Y / z ]. X R z <-> X R Y ) )
9 2 8 ax-mp
 |-  ( [. Y / z ]. X R z <-> X R Y )
10 sbcel1v
 |-  ( [. Y / z ]. z e. A <-> Y e. A )
11 4 9 10 3imtr3g
 |-  ( [. Y / z ]. ( X R z -> z e. A ) -> ( X R Y -> Y e. A ) )
12 3 11 syl
 |-  ( A. z ( X R z -> z e. A ) -> ( X R Y -> Y e. A ) )
13 1 frege71
 |-  ( ( A. z ( X R z -> z e. A ) -> ( X R Y -> Y e. A ) ) -> ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) ) )
14 12 13 ax-mp
 |-  ( R hereditary A -> ( X e. A -> ( X R Y -> Y e. A ) ) )