Metamath Proof Explorer


Theorem dfuzi

Description: An expression for the upper integers that start at N that is analogous to dfnn2 for positive integers. (Contributed by NM, 6-Jul-2005) (Proof shortened by Mario Carneiro, 3-May-2014)

Ref Expression
Hypothesis dfuzi.1 N
Assertion dfuzi z | N z = x | N x y x y + 1 x

Proof

Step Hyp Ref Expression
1 dfuzi.1 N
2 ssintab z | N z x | N x y x y + 1 x x N x y x y + 1 x z | N z x
3 1 peano5uzi N x y x y + 1 x z | N z x
4 2 3 mpgbir z | N z x | N x y x y + 1 x
5 1 zrei N
6 5 leidi N N
7 breq2 z = N N z N N
8 7 elrab N z | N z N N N
9 1 6 8 mpbir2an N z | N z
10 peano2uz2 N y z | N z y + 1 z | N z
11 1 10 mpan y z | N z y + 1 z | N z
12 11 rgen y z | N z y + 1 z | N z
13 zex V
14 13 rabex z | N z V
15 eleq2 x = z | N z N x N z | N z
16 eleq2 x = z | N z y + 1 x y + 1 z | N z
17 16 raleqbi1dv x = z | N z y x y + 1 x y z | N z y + 1 z | N z
18 15 17 anbi12d x = z | N z N x y x y + 1 x N z | N z y z | N z y + 1 z | N z
19 14 18 elab z | N z x | N x y x y + 1 x N z | N z y z | N z y + 1 z | N z
20 9 12 19 mpbir2an z | N z x | N x y x y + 1 x
21 intss1 z | N z x | N x y x y + 1 x x | N x y x y + 1 x z | N z
22 20 21 ax-mp x | N x y x y + 1 x z | N z
23 4 22 eqssi z | N z = x | N x y x y + 1 x