Metamath Proof Explorer


Theorem uzind4s

Description: Induction on the upper set of integers that starts at an integer M , using explicit substitution. The hypotheses are the basis and the induction step. (Contributed by NM, 4-Nov-2005)

Ref Expression
Hypotheses uzind4s.1 M[˙M/k]˙φ
uzind4s.2 kMφ[˙k+1/k]˙φ
Assertion uzind4s NM[˙N/k]˙φ

Proof

Step Hyp Ref Expression
1 uzind4s.1 M[˙M/k]˙φ
2 uzind4s.2 kMφ[˙k+1/k]˙φ
3 dfsbcq2 j=Mjkφ[˙M/k]˙φ
4 sbequ j=mjkφmkφ
5 dfsbcq2 j=m+1jkφ[˙m+1/k]˙φ
6 dfsbcq2 j=Njkφ[˙N/k]˙φ
7 nfv kmM
8 nfs1v kmkφ
9 nfsbc1v k[˙m+1/k]˙φ
10 8 9 nfim kmkφ[˙m+1/k]˙φ
11 7 10 nfim kmMmkφ[˙m+1/k]˙φ
12 eleq1w k=mkMmM
13 sbequ12 k=mφmkφ
14 oveq1 k=mk+1=m+1
15 14 sbceq1d k=m[˙k+1/k]˙φ[˙m+1/k]˙φ
16 13 15 imbi12d k=mφ[˙k+1/k]˙φmkφ[˙m+1/k]˙φ
17 12 16 imbi12d k=mkMφ[˙k+1/k]˙φmMmkφ[˙m+1/k]˙φ
18 11 17 2 chvarfv mMmkφ[˙m+1/k]˙φ
19 3 4 5 6 1 18 uzind4 NM[˙N/k]˙φ