fzennn

Description: The cardinality of a finite set of sequential integers. (See om2uz0i for a description of the hypothesis.) (Contributed by Mario Carneiro, 12-Feb-2013) (Revised by Mario Carneiro, 7-Mar-2014)

		Ref	Expression
	Hypothesis	fzennn.1	$⊢ G = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
	Assertion	fzennn	$⊢ N \in ℕ_{0} \to (1 \dots N) \approx G^{-1} (N)$

Proof

Step	Hyp	Ref	Expression
1		fzennn.1	$⊢ G = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
2		oveq2	$⊢ n = 0 \to (1 \dots n) = (1 \dots 0)$
3		fveq2	$⊢ n = 0 \to G^{-1} (n) = G^{-1} (0)$
4	2 3	breq12d	$⊢ n = 0 \to ((1 \dots n) \approx G^{-1} (n) \leftrightarrow (1 \dots 0) \approx G^{-1} (0))$
5		oveq2	$⊢ n = m \to (1 \dots n) = (1 \dots m)$
6		fveq2	$⊢ n = m \to G^{-1} (n) = G^{-1} (m)$
7	5 6	breq12d	$⊢ n = m \to ((1 \dots n) \approx G^{-1} (n) \leftrightarrow (1 \dots m) \approx G^{-1} (m))$
8		oveq2	$⊢ n = m + 1 \to (1 \dots n) = (1 \dots m + 1)$
9		fveq2	$⊢ n = m + 1 \to G^{-1} (n) = G^{-1} (m + 1)$
10	8 9	breq12d	$⊢ n = m + 1 \to ((1 \dots n) \approx G^{-1} (n) \leftrightarrow (1 \dots m + 1) \approx G^{-1} (m + 1))$
11		oveq2	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
12		fveq2	$⊢ n = N \to G^{-1} (n) = G^{-1} (N)$
13	11 12	breq12d	$⊢ n = N \to ((1 \dots n) \approx G^{-1} (n) \leftrightarrow (1 \dots N) \approx G^{-1} (N))$
14		0ex	$⊢ \emptyset \in V$
15	14	enref	$⊢ \emptyset \approx \emptyset$
16		fz10	$⊢ (1 \dots 0) = \emptyset$
17		0z	$⊢ 0 \in ℤ$
18	17 1	om2uzf1oi	$⊢ G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0}$
19		peano1	$⊢ \emptyset \in ω$
20	18 19	pm3.2i	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0} \land \emptyset \in ω)$
21	17 1	om2uz0i	$⊢ G (\emptyset) = 0$
22		f1ocnvfv	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0} \land \emptyset \in ω) \to (G (\emptyset) = 0 \to G^{-1} (0) = \emptyset)$
23	20 21 22	mp2	$⊢ G^{-1} (0) = \emptyset$
24	15 16 23	3brtr4i	$⊢ (1 \dots 0) \approx G^{-1} (0)$
25		simpr	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to (1 \dots m) \approx G^{-1} (m)$
26		ovex	$⊢ m + 1 \in V$
27		fvex	$⊢ G^{-1} (m) \in V$
28		en2sn	$⊢ (m + 1 \in V \land G^{-1} (m) \in V) \to \{m + 1\} \approx \{G^{-1} (m)\}$
29	26 27 28	mp2an	$⊢ \{m + 1\} \approx \{G^{-1} (m)\}$
30	29	a1i	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to \{m + 1\} \approx \{G^{-1} (m)\}$
31		fzp1disj	$⊢ (1 \dots m) \cap \{m + 1\} = \emptyset$
32	31	a1i	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to (1 \dots m) \cap \{m + 1\} = \emptyset$
33		f1ocnvdm	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0} \land m \in ℤ_{\geq 0}) \to G^{-1} (m) \in ω$
34	18 33	mpan	$⊢ m \in ℤ_{\geq 0} \to G^{-1} (m) \in ω$
35		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
36	34 35	eleq2s	$⊢ m \in ℕ_{0} \to G^{-1} (m) \in ω$
37		nnord	$⊢ G^{-1} (m) \in ω \to Ord G^{-1} (m)$
38		ordirr	$⊢ Ord G^{-1} (m) \to \neg G^{-1} (m) \in G^{-1} (m)$
39	36 37 38	3syl	$⊢ m \in ℕ_{0} \to \neg G^{-1} (m) \in G^{-1} (m)$
40	39	adantr	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to \neg G^{-1} (m) \in G^{-1} (m)$
41		disjsn	$⊢ G^{-1} (m) \cap \{G^{-1} (m)\} = \emptyset \leftrightarrow \neg G^{-1} (m) \in G^{-1} (m)$
42	40 41	sylibr	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to G^{-1} (m) \cap \{G^{-1} (m)\} = \emptyset$
43		unen	$⊢ (((1 \dots m) \approx G^{-1} (m) \land \{m + 1\} \approx \{G^{-1} (m)\}) \land ((1 \dots m) \cap \{m + 1\} = \emptyset \land G^{-1} (m) \cap \{G^{-1} (m)\} = \emptyset)) \to ((1 \dots m) \cup \{m + 1\}) \approx (G^{-1} (m) \cup \{G^{-1} (m)\})$
44	25 30 32 42 43	syl22anc	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to ((1 \dots m) \cup \{m + 1\}) \approx (G^{-1} (m) \cup \{G^{-1} (m)\})$
45		1z	$⊢ 1 \in ℤ$
46		1m1e0	$⊢ 1 - 1 = 0$
47	46	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
48	35 47	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
49	48	eleq2i	$⊢ m \in ℕ_{0} \leftrightarrow m \in ℤ_{\geq (1 - 1)}$
50	49	biimpi	$⊢ m \in ℕ_{0} \to m \in ℤ_{\geq (1 - 1)}$
51		fzsuc2	$⊢ (1 \in ℤ \land m \in ℤ_{\geq (1 - 1)}) \to (1 \dots m + 1) = (1 \dots m) \cup \{m + 1\}$
52	45 50 51	sylancr	$⊢ m \in ℕ_{0} \to (1 \dots m + 1) = (1 \dots m) \cup \{m + 1\}$
53	52	adantr	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to (1 \dots m + 1) = (1 \dots m) \cup \{m + 1\}$
54		peano2	$⊢ G^{-1} (m) \in ω \to suc G^{-1} (m) \in ω$
55	36 54	syl	$⊢ m \in ℕ_{0} \to suc G^{-1} (m) \in ω$
56	55 18	jctil	$⊢ m \in ℕ_{0} \to (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0} \land suc G^{-1} (m) \in ω)$
57	17 1	om2uzsuci	$⊢ G^{-1} (m) \in ω \to G (suc G^{-1} (m)) = G (G^{-1} (m)) + 1$
58	36 57	syl	$⊢ m \in ℕ_{0} \to G (suc G^{-1} (m)) = G (G^{-1} (m)) + 1$
59	35	eleq2i	$⊢ m \in ℕ_{0} \leftrightarrow m \in ℤ_{\geq 0}$
60	59	biimpi	$⊢ m \in ℕ_{0} \to m \in ℤ_{\geq 0}$
61		f1ocnvfv2	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0} \land m \in ℤ_{\geq 0}) \to G (G^{-1} (m)) = m$
62	18 60 61	sylancr	$⊢ m \in ℕ_{0} \to G (G^{-1} (m)) = m$
63	62	oveq1d	$⊢ m \in ℕ_{0} \to G (G^{-1} (m)) + 1 = m + 1$
64	58 63	eqtrd	$⊢ m \in ℕ_{0} \to G (suc G^{-1} (m)) = m + 1$
65		f1ocnvfv	$⊢ (G : ω \underset{1-1 onto}{⟶} ℤ_{\geq 0} \land suc G^{-1} (m) \in ω) \to (G (suc G^{-1} (m)) = m + 1 \to G^{-1} (m + 1) = suc G^{-1} (m))$
66	56 64 65	sylc	$⊢ m \in ℕ_{0} \to G^{-1} (m + 1) = suc G^{-1} (m)$
67	66	adantr	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to G^{-1} (m + 1) = suc G^{-1} (m)$
68		df-suc	$⊢ suc G^{-1} (m) = G^{-1} (m) \cup \{G^{-1} (m)\}$
69	67 68	eqtrdi	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to G^{-1} (m + 1) = G^{-1} (m) \cup \{G^{-1} (m)\}$
70	44 53 69	3brtr4d	$⊢ (m \in ℕ_{0} \land (1 \dots m) \approx G^{-1} (m)) \to (1 \dots m + 1) \approx G^{-1} (m + 1)$
71	70	ex	$⊢ m \in ℕ_{0} \to ((1 \dots m) \approx G^{-1} (m) \to (1 \dots m + 1) \approx G^{-1} (m + 1))$
72	4 7 10 13 24 71	nn0ind	$⊢ N \in ℕ_{0} \to (1 \dots N) \approx G^{-1} (N)$

Metamath Proof Explorer

Theorem fzennn

Proof