Metamath Proof Explorer

Theorem frege70

Description: Lemma for frege72 . Proposition 70 of Frege1879 p. 58. (Contributed by RP, 28-Mar-2020) (Revised by RP, 3-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis frege70.x 
|- X e. V
Assertion frege70 
|- ( R hereditary A -> ( X e. A -> A. y ( X R y -> y e. A ) ) )

Proof

Step Hyp Ref Expression
1 frege70.x 
 |-  X e. V
2 dffrege69 
 |-  ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) <-> R hereditary A )
3 1 frege68c 
 |-  ( ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) <-> R hereditary A ) -> ( R hereditary A -> [. X / x ]. ( x e. A -> A. y ( x R y -> y e. A ) ) ) )
4 sbcel1v 
 |-  ( [. X / x ]. x e. A <-> X e. A )
5 4 biimpri 
 |-  ( X e. A -> [. X / x ]. x e. A )
6 sbcim1 
 |-  ( [. X / x ]. ( x e. A -> A. y ( x R y -> y e. A ) ) -> ( [. X / x ]. x e. A -> [. X / x ]. A. y ( x R y -> y e. A ) ) )
7 sbcal 
 |-  ( [. X / x ]. A. y ( x R y -> y e. A ) <-> A. y [. X / x ]. ( x R y -> y e. A ) )
8 sbcim1 
 |-  ( [. X / x ]. ( x R y -> y e. A ) -> ( [. X / x ]. x R y -> [. X / x ]. y e. A ) )
9 sbcbr1g 
 |-  ( X e. V -> ( [. X / x ]. x R y <-> [_ X / x ]_ x R y ) )
10 1 9 ax-mp 
 |-  ( [. X / x ]. x R y <-> [_ X / x ]_ x R y )
11 csbvarg 
 |-  ( X e. V -> [_ X / x ]_ x = X )
12 1 11 ax-mp 
 |-  [_ X / x ]_ x = X
13 12 breq1i 
 |-  ( [_ X / x ]_ x R y <-> X R y )
14 10 13 bitri 
 |-  ( [. X / x ]. x R y <-> X R y )
15 sbcg 
 |-  ( X e. V -> ( [. X / x ]. y e. A <-> y e. A ) )
16 1 15 ax-mp 
 |-  ( [. X / x ]. y e. A <-> y e. A )
17 8 14 16 3imtr3g 
 |-  ( [. X / x ]. ( x R y -> y e. A ) -> ( X R y -> y e. A ) )
18 17 alimi 
 |-  ( A. y [. X / x ]. ( x R y -> y e. A ) -> A. y ( X R y -> y e. A ) )
19 7 18 sylbi 
 |-  ( [. X / x ]. A. y ( x R y -> y e. A ) -> A. y ( X R y -> y e. A ) )
20 5 6 19 syl56 
 |-  ( [. X / x ]. ( x e. A -> A. y ( x R y -> y e. A ) ) -> ( X e. A -> A. y ( X R y -> y e. A ) ) )
21 3 20 syl6 
 |-  ( ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) <-> R hereditary A ) -> ( R hereditary A -> ( X e. A -> A. y ( X R y -> y e. A ) ) ) )
22 2 21 ax-mp 
 |-  ( R hereditary A -> ( X e. A -> A. y ( X R y -> y e. A ) ) )