Metamath Proof Explorer

Theorem prednn

Description: The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013)

Ref Expression
Assertion prednn 
|- ( N e. NN -> Pred ( < , NN , N ) = ( 1 ... ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 predeq2 
 |-  ( NN = ( ZZ>= ` 1 ) -> Pred ( < , NN , N ) = Pred ( < , ( ZZ>= ` 1 ) , N ) )
3 1 2 ax-mp 
 |-  Pred ( < , NN , N ) = Pred ( < , ( ZZ>= ` 1 ) , N )
4 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
5 preduz 
 |-  ( N e. ( ZZ>= ` 1 ) -> Pred ( < , ( ZZ>= ` 1 ) , N ) = ( 1 ... ( N - 1 ) ) )
6 4 5 sylbi 
 |-  ( N e. NN -> Pred ( < , ( ZZ>= ` 1 ) , N ) = ( 1 ... ( N - 1 ) ) )
7 3 6 eqtrid 
 |-  ( N e. NN -> Pred ( < , NN , N ) = ( 1 ... ( N - 1 ) ) )