This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V ⟼ x + 1), 0) ↾}_{ω}$
	Assertion	cardfz	$⊢ N \in ℕ_{0} \to card ((1 \dots N)) = G^{-1} (N)$

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	$⊢ G = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
2	1	fzennn	$⊢ N \in ℕ_{0} \to (1 \dots N) \approx G^{-1} (N)$
3		carden2b	$⊢ (1 \dots N) \approx G^{-1} (N) \to card ((1 \dots N)) = card (G^{-1} (N))$
4	2 3	syl	$⊢ N \in ℕ_{0} \to card ((1 \dots N)) = card (G^{-1} (N))$
5		0z	$⊢ 0 \in ℤ$
6	5 1	om2uzf1oi	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0}$
7		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
8	7	biimpi	$⊢ N \in ℕ_{0} \to N \in ℤ_{\geq 0}$
9		f1ocnvdm	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0} \land N \in ℤ_{\geq 0}) \to G^{-1} (N) \in ω$
10	6 8 9	sylancr	$⊢ N \in ℕ_{0} \to G^{-1} (N) \in ω$
11		cardnn	$⊢ G^{-1} (N) \in ω \to card (G^{-1} (N)) = G^{-1} (N)$
12	10 11	syl	$⊢ N \in ℕ_{0} \to card (G^{-1} (N)) = G^{-1} (N)$
13	4 12	eqtrd	$⊢ N \in ℕ_{0} \to card ((1 \dots N)) = G^{-1} (N)$