Metamath Proof Explorer


Theorem unblem3

Description: Lemma for unbnn . The value of the function F is less than its value at a successor. (Contributed by NM, 3-Dec-2003)

Ref Expression
Hypothesis unblem.2 F=recxVAsucxAω
Assertion unblem3 AωwωvAwvzωFzFsucz

Proof

Step Hyp Ref Expression
1 unblem.2 F=recxVAsucxAω
2 1 unblem2 AωwωvAwvzωFzA
3 2 imp AωwωvAwvzωFzA
4 omsson ωOn
5 sstr AωωOnAOn
6 4 5 mpan2 AωAOn
7 ssel AOnFzAFzOn
8 7 anc2li AOnFzAAOnFzOn
9 6 8 syl AωFzAAOnFzOn
10 9 ad2antrr AωwωvAwvzωFzAAOnFzOn
11 3 10 mpd AωwωvAwvzωAOnFzOn
12 onmindif AOnFzOnFzAsucFz
13 11 12 syl AωwωvAwvzωFzAsucFz
14 unblem1 AωwωvAwvFzAAsucFzA
15 14 ex AωwωvAwvFzAAsucFzA
16 2 15 syld AωwωvAwvzωAsucFzA
17 suceq y=xsucy=sucx
18 17 difeq2d y=xAsucy=Asucx
19 18 inteqd y=xAsucy=Asucx
20 suceq y=Fzsucy=sucFz
21 20 difeq2d y=FzAsucy=AsucFz
22 21 inteqd y=FzAsucy=AsucFz
23 1 19 22 frsucmpt2 zωAsucFzAFsucz=AsucFz
24 23 ex zωAsucFzAFsucz=AsucFz
25 16 24 sylcom AωwωvAwvzωFsucz=AsucFz
26 25 imp AωwωvAwvzωFsucz=AsucFz
27 13 26 eleqtrrd AωwωvAwvzωFzFsucz
28 27 ex AωwωvAwvzωFzFsucz