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 ) ) ) ) ) )