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 e. ZZ
Assertion	dfuzi	|- { z e. ZZ | N <_ z } = |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }

Proof

Step	Hyp	Ref	Expression
1		dfuzi.1	|- N e. ZZ
2		ssintab	|- ( { z e. ZZ | N <_ z } C_ |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> A. x ( ( N e. x /\ A. y e. x ( y + 1 ) e. x ) -> { z e. ZZ | N <_ z } C_ x ) )
3	1	peano5uzi	|- ( ( N e. x /\ A. y e. x ( y + 1 ) e. x ) -> { z e. ZZ | N <_ z } C_ x )
4	2 3	mpgbir	|- { z e. ZZ | N <_ z } C_ |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }
5	1	zrei	|- N e. RR
6	5	leidi	|- N <_ N
7		breq2	|- ( z = N -> ( N <_ z <-> N <_ N ) )
8	7	elrab	|- ( N e. { z e. ZZ | N <_ z } <-> ( N e. ZZ /\ N <_ N ) )
9	1 6 8	mpbir2an	|- N e. { z e. ZZ | N <_ z }
10		peano2uz2	|- ( ( N e. ZZ /\ y e. { z e. ZZ | N <_ z } ) -> ( y + 1 ) e. { z e. ZZ | N <_ z } )
11	1 10	mpan	|- ( y e. { z e. ZZ | N <_ z } -> ( y + 1 ) e. { z e. ZZ | N <_ z } )
12	11	rgen	|- A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z }
13		zex	|- ZZ e. _V
14	13	rabex	|- { z e. ZZ | N <_ z } e. _V
15		eleq2	|- ( x = { z e. ZZ | N <_ z } -> ( N e. x <-> N e. { z e. ZZ | N <_ z } ) )
16		eleq2	|- ( x = { z e. ZZ | N <_ z } -> ( ( y + 1 ) e. x <-> ( y + 1 ) e. { z e. ZZ | N <_ z } ) )
17	16	raleqbi1dv	|- ( x = { z e. ZZ | N <_ z } -> ( A. y e. x ( y + 1 ) e. x <-> A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z } ) )
18	15 17	anbi12d	|- ( x = { z e. ZZ | N <_ z } -> ( ( N e. x /\ A. y e. x ( y + 1 ) e. x ) <-> ( N e. { z e. ZZ | N <_ z } /\ A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z } ) ) )
19	14 18	elab	|- ( { z e. ZZ | N <_ z } e. { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } <-> ( N e. { z e. ZZ | N <_ z } /\ A. y e. { z e. ZZ | N <_ z } ( y + 1 ) e. { z e. ZZ | N <_ z } ) )
20	9 12 19	mpbir2an	|- { z e. ZZ | N <_ z } e. { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }
21		intss1	|- ( { z e. ZZ | N <_ z } e. { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } -> |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ { z e. ZZ | N <_ z } )
22	20 21	ax-mp	|- |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) } C_ { z e. ZZ | N <_ z }
23	4 22	eqssi	|- { z e. ZZ | N <_ z } = |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }