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	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	cardfz	$$⊢N\in {\mathbb{N}}_0\to \mathrm{card}\left(\left(1\dots N\right)\right)=G^{-1}\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	$$⊢G={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
2	1	fzennn	$$⊢N\in {\mathbb{N}}_0\to \left(1\dots N\right)\approx G^{-1}\left(N\right)$$
3		carden2b	$$⊢\left(1\dots N\right)\approx G^{-1}\left(N\right)\to \mathrm{card}\left(\left(1\dots N\right)\right)=\mathrm{card}\left(G^{-1}\left(N\right)\right)$$
4	2 3	syl	$$⊢N\in {\mathbb{N}}_0\to \mathrm{card}\left(\left(1\dots N\right)\right)=\mathrm{card}\left(G^{-1}\left(N\right)\right)$$
5		0z	$$⊢0\in \mathbb{Z}$$
6	5 1	om2uzf1oi	$$⊢G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{Z}}_{\ge 0}$$
7		elnn0uz	$$⊢N\in {\mathbb{N}}_0\leftrightarrow N\in {\mathbb{Z}}_{\ge 0}$$
8	7	biimpi	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{Z}}_{\ge 0}$$
9		f1ocnvdm	$$⊢\left(G:\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{Z}}_{\ge 0}\wedge N\in {\mathbb{Z}}_{\ge 0}\right)\to G^{-1}\left(N\right)\in \mathrm{\omega }$$
10	6 8 9	sylancr	$$⊢N\in {\mathbb{N}}_0\to G^{-1}\left(N\right)\in \mathrm{\omega }$$
11		cardnn	$$⊢G^{-1}\left(N\right)\in \mathrm{\omega }\to \mathrm{card}\left(G^{-1}\left(N\right)\right)=G^{-1}\left(N\right)$$
12	10 11	syl	$$⊢N\in {\mathbb{N}}_0\to \mathrm{card}\left(G^{-1}\left(N\right)\right)=G^{-1}\left(N\right)$$
13	4 12	eqtrd	$$⊢N\in {\mathbb{N}}_0\to \mathrm{card}\left(\left(1\dots N\right)\right)=G^{-1}\left(N\right)$$