Theorem omsinds

Description: Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015)

	Ref	Expression
Hypotheses	omsinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	omsinds.2	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
	omsinds.3	$$⊢x\in \mathrm{\omega }\to \left(\forall y\in x\psi \to \phi \right)$$
Assertion	omsinds	$$⊢A\in \mathrm{\omega }\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		omsinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		omsinds.2	$$⊢x=A\to \left(\phi \leftrightarrow \chi \right)$$
3		omsinds.3	$$⊢x\in \mathrm{\omega }\to \left(\forall y\in x\psi \to \phi \right)$$
4		omsson	$$⊢\mathrm{\omega }\subseteq \mathrm{On}$$
5		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
6		wess	$$⊢\mathrm{\omega }\subseteq \mathrm{On}\to \left(\mathrm{E}\mathrm{We}\mathrm{On}\to \mathrm{E}\mathrm{We}\mathrm{\omega }\right)$$
7	4 5 6	mp2	$$⊢\mathrm{E}\mathrm{We}\mathrm{\omega }$$
8		epse	$$⊢\mathrm{E}\mathrm{Se}\mathrm{\omega }$$
9		predep	$$⊢x\in \mathrm{\omega }\to Pred\left(\mathrm{E},\mathrm{\omega },x\right)=\mathrm{\omega }\cap x$$
10		ordom	$$⊢\mathrm{Ord}\mathrm{\omega }$$
11		ordtr	$$⊢\mathrm{Ord}\mathrm{\omega }\to \mathrm{Tr}\mathrm{\omega }$$
12		trss	$$⊢\mathrm{Tr}\mathrm{\omega }\to \left(x\in \mathrm{\omega }\to x\subseteq \mathrm{\omega }\right)$$
13	10 11 12	mp2b	$$⊢x\in \mathrm{\omega }\to x\subseteq \mathrm{\omega }$$
14		sseqin2	$$⊢x\subseteq \mathrm{\omega }\leftrightarrow \mathrm{\omega }\cap x=x$$
15	13 14	sylib	$$⊢x\in \mathrm{\omega }\to \mathrm{\omega }\cap x=x$$
16	9 15	eqtrd	$$⊢x\in \mathrm{\omega }\to Pred\left(\mathrm{E},\mathrm{\omega },x\right)=x$$
17	16	raleqdv	$$⊢x\in \mathrm{\omega }\to \left(\forall y\in Pred\left(\mathrm{E},\mathrm{\omega },x\right)\psi \leftrightarrow \forall y\in x\psi \right)$$
18	17 3	sylbid	$$⊢x\in \mathrm{\omega }\to \left(\forall y\in Pred\left(\mathrm{E},\mathrm{\omega },x\right)\psi \to \phi \right)$$
19	7 8 1 2 18	wfis3	$$⊢A\in \mathrm{\omega }\to \chi$$