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 -> ( ph <-> ps ) )
	uzsinds.2	|- ( x = N -> ( ph <-> ch ) )
	uzsinds.3	|- ( x e. ( ZZ>= ` M ) -> ( A. y e. ( M ... ( x - 1 ) ) ps -> ph ) )
Assertion	uzsinds	|- ( N e. ( ZZ>= ` M ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		uzsinds.1	|- ( x = y -> ( ph <-> ps ) )
2		uzsinds.2	|- ( x = N -> ( ph <-> ch ) )
3		uzsinds.3	|- ( x e. ( ZZ>= ` M ) -> ( A. y e. ( M ... ( x - 1 ) ) ps -> ph ) )
4		ltweuz	|- < We ( ZZ>= ` M )
5		fvex	|- ( ZZ>= ` M ) e. _V
6		exse	|- ( ( ZZ>= ` M ) e. _V -> < Se ( ZZ>= ` M ) )
7	5 6	ax-mp	|- < Se ( ZZ>= ` M )
8		preduz	|- ( x e. ( ZZ>= ` M ) -> Pred ( < , ( ZZ>= ` M ) , x ) = ( M ... ( x - 1 ) ) )
9	8	raleqdv	|- ( x e. ( ZZ>= ` M ) -> ( A. y e. Pred ( < , ( ZZ>= ` M ) , x ) ps <-> A. y e. ( M ... ( x - 1 ) ) ps ) )
10	9 3	sylbid	|- ( x e. ( ZZ>= ` M ) -> ( A. y e. Pred ( < , ( ZZ>= ` M ) , x ) ps -> ph ) )
11	4 7 1 2 10	wfis3	|- ( N e. ( ZZ>= ` M ) -> ch )