Theorem uzsinds

Description: Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014)

	Ref	Expression
Hypotheses	uzsinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	uzsinds.2	$$⊢x=N\to \left(\phi \leftrightarrow \chi \right)$$
	uzsinds.3	$$⊢x\in {\mathbb{Z}}_{\ge M}\to \left(\forall y\in \left(M\dots x-1\right)\psi \to \phi \right)$$
Assertion	uzsinds	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		uzsinds.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		uzsinds.2	$$⊢x=N\to \left(\phi \leftrightarrow \chi \right)$$
3		uzsinds.3	$$⊢x\in {\mathbb{Z}}_{\ge M}\to \left(\forall y\in \left(M\dots x-1\right)\psi \to \phi \right)$$
4		ltweuz	$$⊢<\mathrm{We}{\mathbb{Z}}_{\ge M}$$
5		fvex	$$⊢{\mathbb{Z}}_{\ge M}\in \mathrm{V}$$
6		exse	$$⊢{\mathbb{Z}}_{\ge M}\in \mathrm{V}\to <\mathrm{Se}{\mathbb{Z}}_{\ge M}$$
7	5 6	ax-mp	$$⊢<\mathrm{Se}{\mathbb{Z}}_{\ge M}$$
8		preduz	$$⊢x\in {\mathbb{Z}}_{\ge M}\to Pred\left(<,{\mathbb{Z}}_{\ge M},x\right)=\left(M\dots x-1\right)$$
9	8	raleqdv	$$⊢x\in {\mathbb{Z}}_{\ge M}\to \left(\forall y\in Pred\left(<,{\mathbb{Z}}_{\ge M},x\right)\psi \leftrightarrow \forall y\in \left(M\dots x-1\right)\psi \right)$$
10	9 3	sylbid	$$⊢x\in {\mathbb{Z}}_{\ge M}\to \left(\forall y\in Pred\left(<,{\mathbb{Z}}_{\ge M},x\right)\psi \to \phi \right)$$
11	4 7 1 2 10	wfis3	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \chi$$