Metamath Proof Explorer

Theorem frinsg

Description: Well-Founded Induction Schema. If a property passes from all elements less than y of a well-founded class A to y itself (induction hypothesis), then the property holds for all elements of A . Theorem 5.6(ii) of Levy p. 64. (Contributed by Scott Fenton, 7-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypothesis frinsg.1 
|- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
Assertion frinsg 
|- ( ( R Fr A /\ R Se A ) -> A. y e. A ph )

Proof

Step Hyp Ref Expression
1 frinsg.1 
 |-  ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
2 ssrab2 
 |-  { y e. A | ph } C_ A
3 dfss3 
 |-  ( Pred ( R , A , w ) C_ { y e. A | ph } <-> A. z e. Pred ( R , A , w ) z e. { y e. A | ph } )
4 nfcv 
 |-  F/_ y A
5 4 elrabsf 
 |-  ( z e. { y e. A | ph } <-> ( z e. A /\ [. z / y ]. ph ) )
6 5 simprbi 
 |-  ( z e. { y e. A | ph } -> [. z / y ]. ph )
7 6 ralimi 
 |-  ( A. z e. Pred ( R , A , w ) z e. { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph )
8 3 7 sylbi 
 |-  ( Pred ( R , A , w ) C_ { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph )
9 nfv 
 |-  F/ y w e. A
10 nfcv 
 |-  F/_ y Pred ( R , A , w )
11 nfsbc1v 
 |-  F/ y [. z / y ]. ph
12 10 11 nfralw 
 |-  F/ y A. z e. Pred ( R , A , w ) [. z / y ]. ph
13 nfsbc1v 
 |-  F/ y [. w / y ]. ph
14 12 13 nfim 
 |-  F/ y ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph )
15 9 14 nfim 
 |-  F/ y ( w e. A -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) )
16 eleq1w 
 |-  ( y = w -> ( y e. A <-> w e. A ) )
17 predeq3 
 |-  ( y = w -> Pred ( R , A , y ) = Pred ( R , A , w ) )
18 17 raleqdv 
 |-  ( y = w -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph <-> A. z e. Pred ( R , A , w ) [. z / y ]. ph ) )
19 sbceq1a 
 |-  ( y = w -> ( ph <-> [. w / y ]. ph ) )
20 18 19 imbi12d 
 |-  ( y = w -> ( ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) <-> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) )
21 16 20 imbi12d 
 |-  ( y = w -> ( ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) <-> ( w e. A -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) ) )
22 15 21 1 chvarfv 
 |-  ( w e. A -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) )
23 8 22 syl5 
 |-  ( w e. A -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> [. w / y ]. ph ) )
24 23 anc2li 
 |-  ( w e. A -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> ( w e. A /\ [. w / y ]. ph ) ) )
25 4 elrabsf 
 |-  ( w e. { y e. A | ph } <-> ( w e. A /\ [. w / y ]. ph ) )
26 24 25 imbitrrdi 
 |-  ( w e. A -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) )
27 26 rgen 
 |-  A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } )
28 frind 
 |-  ( ( ( R Fr A /\ R Se A ) /\ ( { y e. A | ph } C_ A /\ A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) ) ) -> A = { y e. A | ph } )
29 2 27 28 mpanr12 
 |-  ( ( R Fr A /\ R Se A ) -> A = { y e. A | ph } )
30 rabid2 
 |-  ( A = { y e. A | ph } <-> A. y e. A ph )
31 29 30 sylib 
 |-  ( ( R Fr A /\ R Se A ) -> A. y e. A ph )