Theorem wfisg

Description: Well-Ordered Induction Schema. If a property passes from all elements less than y of a well-ordered class A to y itself (induction hypothesis), then the property holds for all elements of A . (Contributed by Scott Fenton, 11-Feb-2011) (Proof shortened by Scott Fenton, 17-Nov-2024)

	Ref	Expression
Hypothesis	wfisg.1	$$⊢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	wfisg	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to \forall y\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		wfisg.1	$$⊢y\in A\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)$$
2		wefr	$$⊢R\mathrm{We}A\to R\mathrm{Fr}A$$
3	2	adantr	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to R\mathrm{Fr}A$$
4		weso	$$⊢R\mathrm{We}A\to R\mathrm{Or}A$$
5		sopo	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$
6	4 5	syl	$$⊢R\mathrm{We}A\to R\mathrm{Po}A$$
7	6	adantr	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to R\mathrm{Po}A$$
8		simpr	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to R\mathrm{Se}A$$
9	1	adantl	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Po}A\wedge R\mathrm{Se}A\right)\wedge y\in A\right)\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)$$
10	9	frpoinsg	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Po}A\wedge R\mathrm{Se}A\right)\to \forall y\in A\phi$$
11	3 7 8 10	syl3anc	$$⊢\left(R\mathrm{We}A\wedge R\mathrm{Se}A\right)\to \forall y\in A\phi$$