fseq1m1p1

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

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

Proof

Step	Hyp	Ref	Expression
1		fseq1m1p1.1	$⊢ H = \{⟨N, B⟩\}$
2		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
3		eqid	$⊢ \{⟨N - 1 + 1, B⟩\} = \{⟨N - 1 + 1, B⟩\}$
4	3	fseq1p1m1	$⊢ N - 1 \in ℕ_{0} \to ((F : (1 \dots N - 1) ⟶ A \land B \in A \land G = F \cup \{⟨N - 1 + 1, B⟩\}) \leftrightarrow (G : (1 \dots N - 1 + 1) ⟶ A \land G (N - 1 + 1) = B \land F = {G ↾}_{(1 \dots N - 1)}))$
5	2 4	syl	$⊢ N \in ℕ \to ((F : (1 \dots N - 1) ⟶ A \land B \in A \land G = F \cup \{⟨N - 1 + 1, B⟩\}) \leftrightarrow (G : (1 \dots N - 1 + 1) ⟶ A \land G (N - 1 + 1) = B \land F = {G ↾}_{(1 \dots N - 1)}))$
6		nncn	$⊢ N \in ℕ \to N \in ℂ$
7		ax-1cn	$⊢ 1 \in ℂ$
8		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
9	6 7 8	sylancl	$⊢ N \in ℕ \to N - 1 + 1 = N$
10	9	opeq1d	$⊢ N \in ℕ \to ⟨N - 1 + 1, B⟩ = ⟨N, B⟩$
11	10	sneqd	$⊢ N \in ℕ \to \{⟨N - 1 + 1, B⟩\} = \{⟨N, B⟩\}$
12	11 1	eqtr4di	$⊢ N \in ℕ \to \{⟨N - 1 + 1, B⟩\} = H$
13	12	uneq2d	$⊢ N \in ℕ \to F \cup \{⟨N - 1 + 1, B⟩\} = F \cup H$
14	13	eqeq2d	$⊢ N \in ℕ \to (G = F \cup \{⟨N - 1 + 1, B⟩\} \leftrightarrow G = F \cup H)$
15	14	3anbi3d	$⊢ N \in ℕ \to ((F : (1 \dots N - 1) ⟶ A \land B \in A \land G = F \cup \{⟨N - 1 + 1, B⟩\}) \leftrightarrow (F : (1 \dots N - 1) ⟶ A \land B \in A \land G = F \cup H))$
16	9	oveq2d	$⊢ N \in ℕ \to (1 \dots N - 1 + 1) = (1 \dots N)$
17	16	feq2d	$⊢ N \in ℕ \to (G : (1 \dots N - 1 + 1) ⟶ A \leftrightarrow G : (1 \dots N) ⟶ A)$
18	9	fveqeq2d	$⊢ N \in ℕ \to (G (N - 1 + 1) = B \leftrightarrow G (N) = B)$
19	17 18	3anbi12d	$⊢ N \in ℕ \to ((G : (1 \dots N - 1 + 1) ⟶ A \land G (N - 1 + 1) = B \land F = {G ↾}_{(1 \dots N - 1)}) \leftrightarrow (G : (1 \dots N) ⟶ A \land G (N) = B \land F = {G ↾}_{(1 \dots N - 1)}))$
20	5 15 19	3bitr3d	$⊢ N \in ℕ \to ((F : (1 \dots N - 1) ⟶ A \land B \in A \land G = F \cup H) \leftrightarrow (G : (1 \dots N) ⟶ A \land G (N) = B \land F = {G ↾}_{(1 \dots N - 1)}))$

Metamath Proof Explorer

Theorem fseq1m1p1

Proof