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	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	uzsinds.2	⊢ ( 𝑥 = 𝑁 → ( 𝜑 ↔ 𝜒 ) )
	uzsinds.3	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑦 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) )
Assertion	uzsinds	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		uzsinds.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		uzsinds.2	⊢ ( 𝑥 = 𝑁 → ( 𝜑 ↔ 𝜒 ) )
3		uzsinds.3	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑦 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) 𝜓 → 𝜑 ) )
4		ltweuz	⊢ < We ( ℤ≥ ‘ 𝑀 )
5		fvex	⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
6		exse	⊢ ( ( ℤ≥ ‘ 𝑀 ) ∈ V → < Se ( ℤ≥ ‘ 𝑀 ) )
7	5 6	ax-mp	⊢ < Se ( ℤ≥ ‘ 𝑀 )
8		preduz	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑥 ) = ( 𝑀 ... ( 𝑥 − 1 ) ) )
9	8	raleqdv	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑦 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑥 ) 𝜓 ↔ ∀ 𝑦 ∈ ( 𝑀 ... ( 𝑥 − 1 ) ) 𝜓 ) )
10	9 3	sylbid	⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ∀ 𝑦 ∈ Pred ( < , ( ℤ≥ ‘ 𝑀 ) , 𝑥 ) 𝜓 → 𝜑 ) )
11	4 7 1 2 10	wfis3	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝜒 )