This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = { ⟨ 𝑁 , 𝐵 ⟩ }
Assertion fseq1m1p1 ( 𝑁 ∈ ℕ → ( ( 𝐹 : ( 1 ... ( 𝑁 − 1 ) ) ⟶ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = ( 𝐹 ∪ 𝐻 ) ) ↔ ( 𝐺 : ( 1 ... 𝑁 ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑁 ) = 𝐵 ∧ 𝐹 = ( 𝐺 ↾ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fseq1m1p1.1 ⊢ 𝐻 = { ⟨ 𝑁 , 𝐵 ⟩ }
2 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
3 eqid ⊢ { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } = { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ }
4 3 fseq1p1m1 ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 → ( ( 𝐹 : ( 1 ... ( 𝑁 − 1 ) ) ⟶ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = ( 𝐹 ∪ { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } ) ) ↔ ( 𝐺 : ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ ( ( 𝑁 − 1 ) + 1 ) ) = 𝐵 ∧ 𝐹 = ( 𝐺 ↾ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) )
5 2 4 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐹 : ( 1 ... ( 𝑁 − 1 ) ) ⟶ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = ( 𝐹 ∪ { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } ) ) ↔ ( 𝐺 : ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ ( ( 𝑁 − 1 ) + 1 ) ) = 𝐵 ∧ 𝐹 = ( 𝐺 ↾ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) )
6 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
7 ax-1cn ⊢ 1 ∈ ℂ
8 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
9 6 7 8 sylancl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
10 9 opeq1d ⊢ ( 𝑁 ∈ ℕ → ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ = ⟨ 𝑁 , 𝐵 ⟩ )
11 10 sneqd ⊢ ( 𝑁 ∈ ℕ → { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } = { ⟨ 𝑁 , 𝐵 ⟩ } )
12 11 1 eqtr4di ⊢ ( 𝑁 ∈ ℕ → { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } = 𝐻 )
13 12 uneq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ∪ { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } ) = ( 𝐹 ∪ 𝐻 ) )
14 13 eqeq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝐺 = ( 𝐹 ∪ { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } ) ↔ 𝐺 = ( 𝐹 ∪ 𝐻 ) ) )
15 14 3anbi3d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐹 : ( 1 ... ( 𝑁 − 1 ) ) ⟶ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = ( 𝐹 ∪ { ⟨ ( ( 𝑁 − 1 ) + 1 ) , 𝐵 ⟩ } ) ) ↔ ( 𝐹 : ( 1 ... ( 𝑁 − 1 ) ) ⟶ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = ( 𝐹 ∪ 𝐻 ) ) ) )
16 9 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
17 16 feq2d ⊢ ( 𝑁 ∈ ℕ → ( 𝐺 : ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) ⟶ 𝐴 ↔ 𝐺 : ( 1 ... 𝑁 ) ⟶ 𝐴 ) )
18 9 fveqeq2d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐺 ‘ ( ( 𝑁 − 1 ) + 1 ) ) = 𝐵 ↔ ( 𝐺 ‘ 𝑁 ) = 𝐵 ) )
19 17 18 3anbi12d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐺 : ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) ⟶ 𝐴 ∧ ( 𝐺 ‘ ( ( 𝑁 − 1 ) + 1 ) ) = 𝐵 ∧ 𝐹 = ( 𝐺 ↾ ( 1 ... ( 𝑁 − 1 ) ) ) ) ↔ ( 𝐺 : ( 1 ... 𝑁 ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑁 ) = 𝐵 ∧ 𝐹 = ( 𝐺 ↾ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) )
20 5 15 19 3bitr3d ⊢ ( 𝑁 ∈ ℕ → ( ( 𝐹 : ( 1 ... ( 𝑁 − 1 ) ) ⟶ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐺 = ( 𝐹 ∪ 𝐻 ) ) ↔ ( 𝐺 : ( 1 ... 𝑁 ) ⟶ 𝐴 ∧ ( 𝐺 ‘ 𝑁 ) = 𝐵 ∧ 𝐹 = ( 𝐺 ↾ ( 1 ... ( 𝑁 − 1 ) ) ) ) ) )