Metamath Proof Explorer


Theorem frpoins3g

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 )

Proof

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 )