Theorem prednn

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

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

Proof

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