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 syl6ibr
 |-  ( ( ( 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 )