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 = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
Assertion	cardfz	|- ( N e. NN0 -> ( card ` ( 1 ... N ) ) = ( `' G ` N ) )

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2	1	fzennn	|- ( N e. NN0 -> ( 1 ... N ) ~~ ( `' G ` N ) )
3		carden2b	|- ( ( 1 ... N ) ~~ ( `' G ` N ) -> ( card ` ( 1 ... N ) ) = ( card ` ( `' G ` N ) ) )
4	2 3	syl	|- ( N e. NN0 -> ( card ` ( 1 ... N ) ) = ( card ` ( `' G ` N ) ) )
5		0z	|- 0 e. ZZ
6	5 1	om2uzf1oi	|- G : _om -1-1-onto-> ( ZZ>= ` 0 )
7		elnn0uz	|- ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
8	7	biimpi	|- ( N e. NN0 -> N e. ( ZZ>= ` 0 ) )
9		f1ocnvdm	|- ( ( G : _om -1-1-onto-> ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` 0 ) ) -> ( `' G ` N ) e. _om )
10	6 8 9	sylancr	|- ( N e. NN0 -> ( `' G ` N ) e. _om )
11		cardnn	|- ( ( `' G ` N ) e. _om -> ( card ` ( `' G ` N ) ) = ( `' G ` N ) )
12	10 11	syl	|- ( N e. NN0 -> ( card ` ( `' G ` N ) ) = ( `' G ` N ) )
13	4 12	eqtrd	|- ( N e. NN0 -> ( card ` ( 1 ... N ) ) = ( `' G ` N ) )