Metamath Proof Explorer


Theorem wfis

Description: Well-Ordered Induction Schema. If all elements less than a given set x of the well-ordered class A have a property (induction hypothesis), then all elements of A have that property. (Contributed by Scott Fenton, 29-Jan-2011)

Ref Expression
Hypotheses wfis.1 R We A
wfis.2 R Se A
wfis.3 y A z Pred R A y [˙z / y]˙ φ φ
Assertion wfis y A φ

Proof

Step Hyp Ref Expression
1 wfis.1 R We A
2 wfis.2 R Se A
3 wfis.3 y A z Pred R A y [˙z / y]˙ φ φ
4 3 wfisg R We A R Se A y A φ
5 1 2 4 mp2an y A φ
6 5 rspec y A φ