Metamath Proof Explorer

Theorem 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 ∈ ℕ → F : 1 … N − 1 ⟶ A ∧ B ∈ A ∧ G = F ∪ H ↔ G : 1 … N ⟶ A ∧ G ⁡ N = B ∧ F = G ↾ 1 … N − 1

Proof

Step Hyp Ref Expression
1 fseq1m1p1.1 ⊢ H = N B
2 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
3 eqid ⊢ N - 1 + 1 B = N - 1 + 1 B
4 3 fseq1p1m1 ⊢ N − 1 ∈ ℕ 0 → F : 1 … N − 1 ⟶ A ∧ B ∈ A ∧ G = F ∪ N - 1 + 1 B ↔ G : 1 … N - 1 + 1 ⟶ A ∧ G ⁡ N - 1 + 1 = B ∧ F = G ↾ 1 … N − 1
5 2 4 syl ⊢ N ∈ ℕ → F : 1 … N − 1 ⟶ A ∧ B ∈ A ∧ G = F ∪ N - 1 + 1 B ↔ G : 1 … N - 1 + 1 ⟶ A ∧ G ⁡ N - 1 + 1 = B ∧ F = G ↾ 1 … N − 1
6 nncn ⊢ N ∈ ℕ → N ∈ ℂ
7 ax-1cn ⊢ 1 ∈ ℂ
8 npcan ⊢ N ∈ ℂ ∧ 1 ∈ ℂ → N - 1 + 1 = N
9 6 7 8 sylancl ⊢ N ∈ ℕ → N - 1 + 1 = N
10 9 opeq1d ⊢ N ∈ ℕ → N - 1 + 1 B = N B
11 10 sneqd ⊢ N ∈ ℕ → N - 1 + 1 B = N B
12 11 1 eqtr4di ⊢ N ∈ ℕ → N - 1 + 1 B = H
13 12 uneq2d ⊢ N ∈ ℕ → F ∪ N - 1 + 1 B = F ∪ H
14 13 eqeq2d ⊢ N ∈ ℕ → G = F ∪ N - 1 + 1 B ↔ G = F ∪ H
15 14 3anbi3d ⊢ N ∈ ℕ → F : 1 … N − 1 ⟶ A ∧ B ∈ A ∧ G = F ∪ N - 1 + 1 B ↔ F : 1 … N − 1 ⟶ A ∧ B ∈ A ∧ G = F ∪ H
16 9 oveq2d ⊢ N ∈ ℕ → 1 … N - 1 + 1 = 1 … N
17 16 feq2d ⊢ N ∈ ℕ → G : 1 … N - 1 + 1 ⟶ A ↔ G : 1 … N ⟶ A
18 9 fveqeq2d ⊢ N ∈ ℕ → G ⁡ N - 1 + 1 = B ↔ G ⁡ N = B
19 17 18 3anbi12d ⊢ N ∈ ℕ → G : 1 … N - 1 + 1 ⟶ A ∧ G ⁡ N - 1 + 1 = B ∧ F = G ↾ 1 … N − 1 ↔ G : 1 … N ⟶ A ∧ G ⁡ N = B ∧ F = G ↾ 1 … N − 1
20 5 15 19 3bitr3d ⊢ N ∈ ℕ → F : 1 … N − 1 ⟶ A ∧ B ∈ A ∧ G = F ∪ H ↔ G : 1 … N ⟶ A ∧ G ⁡ N = B ∧ F = G ↾ 1 … N − 1