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 e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
Assertion	wfis	|- ( y e. A -> ph )

Proof

Step	Hyp	Ref	Expression
1		wfis.1	|- R We A
2		wfis.2	|- R Se A
3		wfis.3	|- ( y e. A -> ( A. z e. Pred ( R , A , y ) [. z / y ]. ph -> ph ) )
4	3	wfisg	|- ( ( R We A /\ R Se A ) -> A. y e. A ph )
5	1 2 4	mp2an	|- A. y e. A ph
6	5	rspec	|- ( y e. A -> ph )