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 x=yφψ
uzsinds.2 x=Nφχ
uzsinds.3 xMyMx1ψφ
Assertion uzsinds NMχ

Proof

Step Hyp Ref Expression
1 uzsinds.1 x=yφψ
2 uzsinds.2 x=Nφχ
3 uzsinds.3 xMyMx1ψφ
4 ltweuz <WeM
5 fvex MV
6 exse MV<SeM
7 5 6 ax-mp <SeM
8 preduz xMPred<Mx=Mx1
9 8 raleqdv xMyPred<MxψyMx1ψ
10 9 3 sylbid xMyPred<Mxψφ
11 4 7 1 2 10 wfis3 NMχ