Theorem prednn0

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

	Ref	Expression
Assertion	prednn0	⊢ ( 𝑁 ∈ ℕ0 → Pred ( < , ℕ0 , 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2		predeq2	⊢ ( ℕ0 = ( ℤ≥ ‘ 0 ) → Pred ( < , ℕ0 , 𝑁 ) = Pred ( < , ( ℤ≥ ‘ 0 ) , 𝑁 ) )
3	1 2	ax-mp	⊢ Pred ( < , ℕ0 , 𝑁 ) = Pred ( < , ( ℤ≥ ‘ 0 ) , 𝑁 )
4		preduz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → Pred ( < , ( ℤ≥ ‘ 0 ) , 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
5	3 4	syl5eq	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → Pred ( < , ℕ0 , 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
6	5 1	eleq2s	⊢ ( 𝑁 ∈ ℕ0 → Pred ( < , ℕ0 , 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )