Metamath Proof Explorer


Theorem preduz

Description: The value of the predecessor class over an upper integer set. (Contributed by Scott Fenton, 16-May-2014)

Ref Expression
Assertion preduz N M Pred < M N = M N 1

Proof

Step Hyp Ref Expression
1 vex x V
2 1 elpred N M x Pred < M N x M x < N
3 eluzelz x M x
4 eluzelz N M N
5 zltlem1 x N x < N x N 1
6 3 4 5 syl2anr N M x M x < N x N 1
7 6 pm5.32da N M x M x < N x M x N 1
8 eluzel2 N M M
9 eluz1 M x M x M x
10 8 9 syl N M x M x M x
11 10 anbi1d N M x M x N 1 x M x x N 1
12 7 11 bitrd N M x M x < N x M x x N 1
13 2 12 bitrd N M x Pred < M N x M x x N 1
14 peano2zm N N 1
15 4 14 syl N M N 1
16 8 15 jca N M M N 1
17 16 biantrurd N M x M x x N 1 M N 1 x M x x N 1
18 13 17 bitrd N M x Pred < M N M N 1 x M x x N 1
19 elfz2 x M N 1 M N 1 x M x x N 1
20 df-3an M N 1 x M N 1 x
21 20 anbi1i M N 1 x M x x N 1 M N 1 x M x x N 1
22 anass M N 1 x M x x N 1 M N 1 x M x x N 1
23 anass x M x x N 1 x M x x N 1
24 23 anbi2i M N 1 x M x x N 1 M N 1 x M x x N 1
25 22 24 bitr4i M N 1 x M x x N 1 M N 1 x M x x N 1
26 19 21 25 3bitri x M N 1 M N 1 x M x x N 1
27 18 26 bitr4di N M x Pred < M N x M N 1
28 27 eqrdv N M Pred < M N = M N 1