Theorem cardfz

Description: The cardinality of a finite set of sequential integers. (See om2uz0i for a description of the hypothesis.) (Contributed by NM, 7-Nov-2008) (Revised by Mario Carneiro, 15-Sep-2013)

	Ref	Expression
Hypothesis	fzennn.1	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
Assertion	cardfz	⊢ ( 𝑁 ∈ ℕ0 → ( card ‘ ( 1 ... 𝑁 ) ) = ( ◡ 𝐺 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2	1	fzennn	⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ≈ ( ◡ 𝐺 ‘ 𝑁 ) )
3		carden2b	⊢ ( ( 1 ... 𝑁 ) ≈ ( ◡ 𝐺 ‘ 𝑁 ) → ( card ‘ ( 1 ... 𝑁 ) ) = ( card ‘ ( ◡ 𝐺 ‘ 𝑁 ) ) )
4	2 3	syl	⊢ ( 𝑁 ∈ ℕ0 → ( card ‘ ( 1 ... 𝑁 ) ) = ( card ‘ ( ◡ 𝐺 ‘ 𝑁 ) ) )
5		0z	⊢ 0 ∈ ℤ
6	5 1	om2uzf1oi	⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 0 )
7		elnn0uz	⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
8	7	biimpi	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
9		f1ocnvdm	⊢ ( ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) → ( ◡ 𝐺 ‘ 𝑁 ) ∈ ω )
10	6 8 9	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( ◡ 𝐺 ‘ 𝑁 ) ∈ ω )
11		cardnn	⊢ ( ( ◡ 𝐺 ‘ 𝑁 ) ∈ ω → ( card ‘ ( ◡ 𝐺 ‘ 𝑁 ) ) = ( ◡ 𝐺 ‘ 𝑁 ) )
12	10 11	syl	⊢ ( 𝑁 ∈ ℕ0 → ( card ‘ ( ◡ 𝐺 ‘ 𝑁 ) ) = ( ◡ 𝐺 ‘ 𝑁 ) )
13	4 12	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( card ‘ ( 1 ... 𝑁 ) ) = ( ◡ 𝐺 ‘ 𝑁 ) )