fseq1p1m1

Description: Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 7-Mar-2014)

		Ref	Expression
	Hypothesis	fseq1p1m1.1	$⊢ H = \{⟨N + 1, B⟩\}$
	Assertion	fseq1p1m1	$⊢ N \in ℕ_{0} \to ((F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H) \leftrightarrow (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)}))$

Proof

Step	Hyp	Ref	Expression
1		fseq1p1m1.1	$⊢ H = \{⟨N + 1, B⟩\}$
2		simpr1	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to F : (1 \dots N) ⟶ A$
3		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
4	3	adantr	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to N + 1 \in ℕ$
5		simpr2	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to B \in A$
6		fsng	$⊢ (N + 1 \in ℕ \land B \in A) \to (H : \{N + 1\} ⟶ \{B\} \leftrightarrow H = \{⟨N + 1, B⟩\})$
7	1 6	mpbiri	$⊢ (N + 1 \in ℕ \land B \in A) \to H : \{N + 1\} ⟶ \{B\}$
8	4 5 7	syl2anc	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to H : \{N + 1\} ⟶ \{B\}$
9	5	snssd	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to \{B\} \subseteq A$
10	8 9	fssd	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to H : \{N + 1\} ⟶ A$
11		fzp1disj	$⊢ (1 \dots N) \cap \{N + 1\} = \emptyset$
12	11	a1i	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (1 \dots N) \cap \{N + 1\} = \emptyset$
13	2 10 12	fun2d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (F \cup H) : (1 \dots N) \cup \{N + 1\} ⟶ A$
14		1z	$⊢ 1 \in ℤ$
15		simpl	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to N \in ℕ_{0}$
16		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
17		1m1e0	$⊢ 1 - 1 = 0$
18	17	fveq2i	$⊢ ℤ_{\geq (1 - 1)} = ℤ_{\geq 0}$
19	16 18	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (1 - 1)}$
20	15 19	eleqtrdi	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to N \in ℤ_{\geq (1 - 1)}$
21		fzsuc2	$⊢ (1 \in ℤ \land N \in ℤ_{\geq (1 - 1)}) \to (1 \dots N + 1) = (1 \dots N) \cup \{N + 1\}$
22	14 20 21	sylancr	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (1 \dots N + 1) = (1 \dots N) \cup \{N + 1\}$
23	22	eqcomd	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (1 \dots N) \cup \{N + 1\} = (1 \dots N + 1)$
24	23	feq2d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to ((F \cup H) : (1 \dots N) \cup \{N + 1\} ⟶ A \leftrightarrow (F \cup H) : (1 \dots N + 1) ⟶ A)$
25	13 24	mpbid	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (F \cup H) : (1 \dots N + 1) ⟶ A$
26		simpr3	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to G = F \cup H$
27	26	feq1d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (G : (1 \dots N + 1) ⟶ A \leftrightarrow (F \cup H) : (1 \dots N + 1) ⟶ A)$
28	25 27	mpbird	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to G : (1 \dots N + 1) ⟶ A$
29		ovex	$⊢ N + 1 \in V$
30	29	snid	$⊢ N + 1 \in \{N + 1\}$
31		fvres	$⊢ N + 1 \in \{N + 1\} \to ({G ↾}_{\{N + 1\}}) (N + 1) = G (N + 1)$
32	30 31	ax-mp	$⊢ ({G ↾}_{\{N + 1\}}) (N + 1) = G (N + 1)$
33	26	reseq1d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {G ↾}_{\{N + 1\}} = {(F \cup H) ↾}_{\{N + 1\}}$
34		ffn	$⊢ F : (1 \dots N) ⟶ A \to F Fn (1 \dots N)$
35		fnresdisj	$⊢ F Fn (1 \dots N) \to ((1 \dots N) \cap \{N + 1\} = \emptyset \leftrightarrow {F ↾}_{\{N + 1\}} = \emptyset)$
36	2 34 35	3syl	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to ((1 \dots N) \cap \{N + 1\} = \emptyset \leftrightarrow {F ↾}_{\{N + 1\}} = \emptyset)$
37	12 36	mpbid	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {F ↾}_{\{N + 1\}} = \emptyset$
38	37	uneq1d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to ({F ↾}_{\{N + 1\}}) \cup ({H ↾}_{\{N + 1\}}) = \emptyset \cup ({H ↾}_{\{N + 1\}})$
39		resundir	$⊢ {(F \cup H) ↾}_{\{N + 1\}} = ({F ↾}_{\{N + 1\}}) \cup ({H ↾}_{\{N + 1\}})$
40		uncom	$⊢ \emptyset \cup ({H ↾}_{\{N + 1\}}) = ({H ↾}_{\{N + 1\}}) \cup \emptyset$
41		un0	$⊢ ({H ↾}_{\{N + 1\}}) \cup \emptyset = {H ↾}_{\{N + 1\}}$
42	40 41	eqtr2i	$⊢ {H ↾}_{\{N + 1\}} = \emptyset \cup ({H ↾}_{\{N + 1\}})$
43	38 39 42	3eqtr4g	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {(F \cup H) ↾}_{\{N + 1\}} = {H ↾}_{\{N + 1\}}$
44		ffn	$⊢ H : \{N + 1\} ⟶ A \to H Fn \{N + 1\}$
45		fnresdm	$⊢ H Fn \{N + 1\} \to {H ↾}_{\{N + 1\}} = H$
46	10 44 45	3syl	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {H ↾}_{\{N + 1\}} = H$
47	33 43 46	3eqtrd	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {G ↾}_{\{N + 1\}} = H$
48	47	fveq1d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to ({G ↾}_{\{N + 1\}}) (N + 1) = H (N + 1)$
49	1	fveq1i	$⊢ H (N + 1) = \{⟨N + 1, B⟩\} (N + 1)$
50		fvsng	$⊢ (N + 1 \in ℕ \land B \in A) \to \{⟨N + 1, B⟩\} (N + 1) = B$
51	49 50	syl5eq	$⊢ (N + 1 \in ℕ \land B \in A) \to H (N + 1) = B$
52	4 5 51	syl2anc	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to H (N + 1) = B$
53	48 52	eqtrd	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to ({G ↾}_{\{N + 1\}}) (N + 1) = B$
54	32 53	syl5eqr	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to G (N + 1) = B$
55	26	reseq1d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {G ↾}_{(1 \dots N)} = {(F \cup H) ↾}_{(1 \dots N)}$
56		incom	$⊢ \{N + 1\} \cap (1 \dots N) = (1 \dots N) \cap \{N + 1\}$
57	56 12	syl5eq	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to \{N + 1\} \cap (1 \dots N) = \emptyset$
58		ffn	$⊢ H : \{N + 1\} ⟶ \{B\} \to H Fn \{N + 1\}$
59		fnresdisj	$⊢ H Fn \{N + 1\} \to (\{N + 1\} \cap (1 \dots N) = \emptyset \leftrightarrow {H ↾}_{(1 \dots N)} = \emptyset)$
60	8 58 59	3syl	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (\{N + 1\} \cap (1 \dots N) = \emptyset \leftrightarrow {H ↾}_{(1 \dots N)} = \emptyset)$
61	57 60	mpbid	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {H ↾}_{(1 \dots N)} = \emptyset$
62	61	uneq2d	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to ({F ↾}_{(1 \dots N)}) \cup ({H ↾}_{(1 \dots N)}) = ({F ↾}_{(1 \dots N)}) \cup \emptyset$
63		resundir	$⊢ {(F \cup H) ↾}_{(1 \dots N)} = ({F ↾}_{(1 \dots N)}) \cup ({H ↾}_{(1 \dots N)})$
64		un0	$⊢ ({F ↾}_{(1 \dots N)}) \cup \emptyset = {F ↾}_{(1 \dots N)}$
65	64	eqcomi	$⊢ {F ↾}_{(1 \dots N)} = ({F ↾}_{(1 \dots N)}) \cup \emptyset$
66	62 63 65	3eqtr4g	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {(F \cup H) ↾}_{(1 \dots N)} = {F ↾}_{(1 \dots N)}$
67		fnresdm	$⊢ F Fn (1 \dots N) \to {F ↾}_{(1 \dots N)} = F$
68	2 34 67	3syl	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to {F ↾}_{(1 \dots N)} = F$
69	55 66 68	3eqtrrd	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to F = {G ↾}_{(1 \dots N)}$
70	28 54 69	3jca	$⊢ (N \in ℕ_{0} \land (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)) \to (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})$
71		simpr1	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to G : (1 \dots N + 1) ⟶ A$
72		fzssp1	$⊢ (1 \dots N) \subseteq (1 \dots N + 1)$
73		fssres	$⊢ (G : (1 \dots N + 1) ⟶ A \land (1 \dots N) \subseteq (1 \dots N + 1)) \to ({G ↾}_{(1 \dots N)}) : (1 \dots N) ⟶ A$
74	71 72 73	sylancl	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to ({G ↾}_{(1 \dots N)}) : (1 \dots N) ⟶ A$
75		simpr3	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to F = {G ↾}_{(1 \dots N)}$
76	75	feq1d	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to (F : (1 \dots N) ⟶ A \leftrightarrow ({G ↾}_{(1 \dots N)}) : (1 \dots N) ⟶ A)$
77	74 76	mpbird	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to F : (1 \dots N) ⟶ A$
78		simpr2	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to G (N + 1) = B$
79	3	adantr	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to N + 1 \in ℕ$
80		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
81	79 80	eleqtrdi	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to N + 1 \in ℤ_{\geq 1}$
82		eluzfz2	$⊢ N + 1 \in ℤ_{\geq 1} \to N + 1 \in (1 \dots N + 1)$
83	81 82	syl	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to N + 1 \in (1 \dots N + 1)$
84	71 83	ffvelrnd	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to G (N + 1) \in A$
85	78 84	eqeltrrd	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to B \in A$
86		ffn	$⊢ G : (1 \dots N + 1) ⟶ A \to G Fn (1 \dots N + 1)$
87	71 86	syl	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to G Fn (1 \dots N + 1)$
88		fnressn	$⊢ (G Fn (1 \dots N + 1) \land N + 1 \in (1 \dots N + 1)) \to {G ↾}_{\{N + 1\}} = \{⟨N + 1, G (N + 1)⟩\}$
89	87 83 88	syl2anc	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to {G ↾}_{\{N + 1\}} = \{⟨N + 1, G (N + 1)⟩\}$
90		opeq2	$⊢ G (N + 1) = B \to ⟨N + 1, G (N + 1)⟩ = ⟨N + 1, B⟩$
91	90	sneqd	$⊢ G (N + 1) = B \to \{⟨N + 1, G (N + 1)⟩\} = \{⟨N + 1, B⟩\}$
92	78 91	syl	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to \{⟨N + 1, G (N + 1)⟩\} = \{⟨N + 1, B⟩\}$
93	89 92	eqtrd	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to {G ↾}_{\{N + 1\}} = \{⟨N + 1, B⟩\}$
94	93 1	syl6reqr	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to H = {G ↾}_{\{N + 1\}}$
95	75 94	uneq12d	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to F \cup H = ({G ↾}_{(1 \dots N)}) \cup ({G ↾}_{\{N + 1\}})$
96		simpl	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to N \in ℕ_{0}$
97	96 19	eleqtrdi	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to N \in ℤ_{\geq (1 - 1)}$
98	14 97 21	sylancr	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to (1 \dots N + 1) = (1 \dots N) \cup \{N + 1\}$
99	98	reseq2d	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to {G ↾}_{(1 \dots N + 1)} = {G ↾}_{((1 \dots N) \cup \{N + 1\})}$
100		resundi	$⊢ {G ↾}_{((1 \dots N) \cup \{N + 1\})} = ({G ↾}_{(1 \dots N)}) \cup ({G ↾}_{\{N + 1\}})$
101	99 100	syl6req	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to ({G ↾}_{(1 \dots N)}) \cup ({G ↾}_{\{N + 1\}}) = {G ↾}_{(1 \dots N + 1)}$
102		fnresdm	$⊢ G Fn (1 \dots N + 1) \to {G ↾}_{(1 \dots N + 1)} = G$
103	71 86 102	3syl	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to {G ↾}_{(1 \dots N + 1)} = G$
104	95 101 103	3eqtrrd	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to G = F \cup H$
105	77 85 104	3jca	$⊢ (N \in ℕ_{0} \land (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)})) \to (F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H)$
106	70 105	impbida	$⊢ N \in ℕ_{0} \to ((F : (1 \dots N) ⟶ A \land B \in A \land G = F \cup H) \leftrightarrow (G : (1 \dots N + 1) ⟶ A \land G (N + 1) = B \land F = {G ↾}_{(1 \dots N)}))$

Metamath Proof Explorer

Theorem fseq1p1m1

Proof