Description: Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frpoins3g.1 | |- ( x e. A -> ( A. y e. Pred ( R , A , x ) ps -> ph ) ) |
|
frpoins3g.2 | |- ( x = y -> ( ph <-> ps ) ) |
||
frpoins3g.3 | |- ( x = B -> ( ph <-> ch ) ) |
||
Assertion | frpoins3g | |- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ B e. A ) -> ch ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frpoins3g.1 | |- ( x e. A -> ( A. y e. Pred ( R , A , x ) ps -> ph ) ) |
|
2 | frpoins3g.2 | |- ( x = y -> ( ph <-> ps ) ) |
|
3 | frpoins3g.3 | |- ( x = B -> ( ph <-> ch ) ) |
|
4 | 1 2 | frpoins2g | |- ( ( R Fr A /\ R Po A /\ R Se A ) -> A. x e. A ph ) |
5 | 3 | rspccva | |- ( ( A. x e. A ph /\ B e. A ) -> ch ) |
6 | 4 5 | sylan | |- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ B e. A ) -> ch ) |