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 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 ) }