Metamath Proof Explorer

Theorem frpoinsg

Description: Well-Founded Induction Schema (variant). If a property passes from all elements less than y of a well-founded set-like partial order class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 11-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 frpoinsg.1 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. A ) -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
2 dfss3 
 |-  ( Pred ( R , A , w ) C_ { y e. A | ph } <-> A. z e. Pred ( R , A , w ) z e. { y e. A | ph } )
3 nfcv 
 |-  F/_ y A
4 3 elrabsf 
 |-  ( z e. { y e. A | ph } <-> ( z e. A /\ [. z / y ]. ph ) )
5 4 simprbi 
 |-  ( z e. { y e. A | ph } -> [. z / y ]. ph )
6 5 ralimi 
 |-  ( A. z e. Pred ( R , A , w ) z e. { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph )
7 2 6 sylbi 
 |-  ( Pred ( R , A , w ) C_ { y e. A | ph } -> A. z e. Pred ( R , A , w ) [. z / y ]. ph )
8 nfv 
 |-  F/ y ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A )
9 nfcv 
 |-  F/_ y Pred ( R , A , w )
10 nfsbc1v 
 |-  F/ y [. z / y ]. ph
11 9 10 nfralw 
 |-  F/ y A. z e. Pred ( R , A , w ) [. z / y ]. ph
12 nfsbc1v 
 |-  F/ y [. w / y ]. ph
13 11 12 nfim 
 |-  F/ y ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph )
14 8 13 nfim 
 |-  F/ y ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) )
15 eleq1w 
 |-  ( y = w -> ( y e. A <-> w e. A ) )
16 15 anbi2d 
 |-  ( y = w -> ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. A ) <-> ( ( R Fr A /\ R Po A /\ R Se 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 -> ( ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ y e. A ) -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) ) <-> ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) ) ) )
22 14 21 1 chvarfv 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( A. z e. Pred ( R , A , w ) [. z / y ]. ph -> [. w / y ]. ph ) )
23 7 22 syl5 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> [. w / y ]. ph ) )
24 simpr 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> w e. A )
25 23 24 jctild 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> ( w e. A /\ [. w / y ]. ph ) ) )
26 3 elrabsf 
 |-  ( w e. { y e. A | ph } <-> ( w e. A /\ [. w / y ]. ph ) )
27 25 26 imbitrrdi 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ w e. A ) -> ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) )
28 27 ralrimiva 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> A. w e. A ( Pred ( R , A , w ) C_ { y e. A | ph } -> w e. { y e. A | ph } ) )
29 ssrab2 
 |-  { y e. A | ph } C_ A
30 28 29 jctil 
 |-  ( ( R Fr A /\ R Po 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 } ) ) )
31 frpoind 
 |-  ( ( ( R Fr A /\ R Po 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 } )
32 30 31 mpdan 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> A = { y e. A | ph } )
33 rabid2 
 |-  ( A = { y e. A | ph } <-> A. y e. A ph )
34 32 33 sylib 
 |-  ( ( R Fr A /\ R Po A /\ R Se A ) -> A. y e. A ph )