# 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}=\left\{⟨{N},{B}⟩\right\}$
Assertion fseq1m1p1 ${⊢}{N}\in ℕ\to \left(\left({F}:\left(1\dots {N}-1\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)↔\left({G}:\left(1\dots {N}\right)⟶{A}\wedge {G}\left({N}\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}-1\right)}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fseq1m1p1.1 ${⊢}{H}=\left\{⟨{N},{B}⟩\right\}$
2 nnm1nn0 ${⊢}{N}\in ℕ\to {N}-1\in {ℕ}_{0}$
3 eqid ${⊢}\left\{⟨{N}-1+1,{B}⟩\right\}=\left\{⟨{N}-1+1,{B}⟩\right\}$
4 3 fseq1p1m1 ${⊢}{N}-1\in {ℕ}_{0}\to \left(\left({F}:\left(1\dots {N}-1\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup \left\{⟨{N}-1+1,{B}⟩\right\}\right)↔\left({G}:\left(1\dots {N}-1+1\right)⟶{A}\wedge {G}\left({N}-1+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}-1\right)}\right)\right)$
5 2 4 syl ${⊢}{N}\in ℕ\to \left(\left({F}:\left(1\dots {N}-1\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup \left\{⟨{N}-1+1,{B}⟩\right\}\right)↔\left({G}:\left(1\dots {N}-1+1\right)⟶{A}\wedge {G}\left({N}-1+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}-1\right)}\right)\right)$
6 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
7 ax-1cn ${⊢}1\in ℂ$
8 npcan ${⊢}\left({N}\in ℂ\wedge 1\in ℂ\right)\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 \left\{⟨{N}-1+1,{B}⟩\right\}=\left\{⟨{N},{B}⟩\right\}$
12 11 1 syl6eqr ${⊢}{N}\in ℕ\to \left\{⟨{N}-1+1,{B}⟩\right\}={H}$
13 12 uneq2d ${⊢}{N}\in ℕ\to {F}\cup \left\{⟨{N}-1+1,{B}⟩\right\}={F}\cup {H}$
14 13 eqeq2d ${⊢}{N}\in ℕ\to \left({G}={F}\cup \left\{⟨{N}-1+1,{B}⟩\right\}↔{G}={F}\cup {H}\right)$
15 14 3anbi3d ${⊢}{N}\in ℕ\to \left(\left({F}:\left(1\dots {N}-1\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup \left\{⟨{N}-1+1,{B}⟩\right\}\right)↔\left({F}:\left(1\dots {N}-1\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)\right)$
16 9 oveq2d ${⊢}{N}\in ℕ\to \left(1\dots {N}-1+1\right)=\left(1\dots {N}\right)$
17 16 feq2d ${⊢}{N}\in ℕ\to \left({G}:\left(1\dots {N}-1+1\right)⟶{A}↔{G}:\left(1\dots {N}\right)⟶{A}\right)$
18 9 fveqeq2d ${⊢}{N}\in ℕ\to \left({G}\left({N}-1+1\right)={B}↔{G}\left({N}\right)={B}\right)$
19 17 18 3anbi12d ${⊢}{N}\in ℕ\to \left(\left({G}:\left(1\dots {N}-1+1\right)⟶{A}\wedge {G}\left({N}-1+1\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}-1\right)}\right)↔\left({G}:\left(1\dots {N}\right)⟶{A}\wedge {G}\left({N}\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}-1\right)}\right)\right)$
20 5 15 19 3bitr3d ${⊢}{N}\in ℕ\to \left(\left({F}:\left(1\dots {N}-1\right)⟶{A}\wedge {B}\in {A}\wedge {G}={F}\cup {H}\right)↔\left({G}:\left(1\dots {N}\right)⟶{A}\wedge {G}\left({N}\right)={B}\wedge {F}={{G}↾}_{\left(1\dots {N}-1\right)}\right)\right)$