Metamath Proof Explorer


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 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝜒 )