This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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