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 | |
|
uzind4s.2 | |
||
Assertion | uzind4s | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzind4s.1 | |
|
2 | uzind4s.2 | |
|
3 | dfsbcq2 | |
|
4 | sbequ | |
|
5 | dfsbcq2 | |
|
6 | dfsbcq2 | |
|
7 | nfv | |
|
8 | nfs1v | |
|
9 | nfsbc1v | |
|
10 | 8 9 | nfim | |
11 | 7 10 | nfim | |
12 | eleq1w | |
|
13 | sbequ12 | |
|
14 | oveq1 | |
|
15 | 14 | sbceq1d | |
16 | 13 15 | imbi12d | |
17 | 12 16 | imbi12d | |
18 | 11 17 2 | chvarfv | |
19 | 3 4 5 6 1 18 | uzind4 | |