Metamath Proof Explorer

Theorem prednn0

Description: The value of the predecessor class over NN0 . (Contributed by Scott Fenton, 9-May-2014)

Ref Expression
Assertion prednn0 
|- ( N e. NN0 -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 predeq2 
 |-  ( NN0 = ( ZZ>= ` 0 ) -> Pred ( < , NN0 , N ) = Pred ( < , ( ZZ>= ` 0 ) , N ) )
3 1 2 ax-mp 
 |-  Pred ( < , NN0 , N ) = Pred ( < , ( ZZ>= ` 0 ) , N )
4 preduz 
 |-  ( N e. ( ZZ>= ` 0 ) -> Pred ( < , ( ZZ>= ` 0 ) , N ) = ( 0 ... ( N - 1 ) ) )
5 3 4 eqtrid 
 |-  ( N e. ( ZZ>= ` 0 ) -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
6 5 1 eleq2s 
 |-  ( N e. NN0 -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )