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\mathrm{We}A$$
	wfis.2	$$⊢R\mathrm{Se}A$$
	wfis.3	$$⊢y\in A\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)$$
Assertion	wfis	$$⊢y\in A\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		wfis.1	$$⊢R\mathrm{We}A$$
2		wfis.2	$$⊢R\mathrm{Se}A$$
3		wfis.3	$$⊢y\in A\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)$$
4	3	wfisg	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to \forall y\in A\phi$$
5	1 2 4	mp2an	$$⊢\forall y\in A\phi$$
6	5	rspec	$$⊢y\in A\to \phi$$