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

Metamath Proof Explorer

Theorem peano5uzti

Description: Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005) (Revised by Mario Carneiro, 25-Jul-2013)

Ref Expression
Assertion peano5uzti 
|- ( N e. ZZ -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( N e. A <-> if ( N e. ZZ , N , 1 ) e. A ) )
2 1 anbi1d 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) <-> ( if ( N e. ZZ , N , 1 ) e. A /\ A. x e. A ( x + 1 ) e. A ) ) )
3 breq1 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( N <_ k <-> if ( N e. ZZ , N , 1 ) <_ k ) )
4 3 rabbidv 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> { k e. ZZ | N <_ k } = { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } )
5 4 sseq1d 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( { k e. ZZ | N <_ k } C_ A <-> { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } C_ A ) )
6 2 5 imbi12d 
 |-  ( N = if ( N e. ZZ , N , 1 ) -> ( ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A ) <-> ( ( if ( N e. ZZ , N , 1 ) e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } C_ A ) ) )
7 1z 
 |-  1 e. ZZ
8 7 elimel 
 |-  if ( N e. ZZ , N , 1 ) e. ZZ
9 8 peano5uzi 
 |-  ( ( if ( N e. ZZ , N , 1 ) e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | if ( N e. ZZ , N , 1 ) <_ k } C_ A )
10 6 9 dedth 
 |-  ( N e. ZZ -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A ) )