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 e. NN -> ( ( F : ( 1 ... ( N - 1 ) ) --> A /\ B e. A /\ G = ( F u. 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 e. NN -> ( N - 1 ) e. NN0 )
3 eqid 
 |-  { <. ( ( N - 1 ) + 1 ) , B >. } = { <. ( ( N - 1 ) + 1 ) , B >. }
4 3 fseq1p1m1 
 |-  ( ( N - 1 ) e. NN0 -> ( ( F : ( 1 ... ( N - 1 ) ) --> A /\ B e. A /\ G = ( F u. { <. ( ( 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 e. NN -> ( ( F : ( 1 ... ( N - 1 ) ) --> A /\ B e. A /\ G = ( F u. { <. ( ( N - 1 ) + 1 ) , B >. } ) ) <-> ( G : ( 1 ... ( ( N - 1 ) + 1 ) ) --> A /\ ( G ` ( ( N - 1 ) + 1 ) ) = B /\ F = ( G |` ( 1 ... ( N - 1 ) ) ) ) ) )
6 nncn 
 |-  ( N e. NN -> N e. CC )
7 ax-1cn 
 |-  1 e. CC
8 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
9 6 7 8 sylancl 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
10 9 opeq1d 
 |-  ( N e. NN -> <. ( ( N - 1 ) + 1 ) , B >. = <. N , B >. )
11 10 sneqd 
 |-  ( N e. NN -> { <. ( ( N - 1 ) + 1 ) , B >. } = { <. N , B >. } )
12 11 1 eqtr4di 
 |-  ( N e. NN -> { <. ( ( N - 1 ) + 1 ) , B >. } = H )
13 12 uneq2d 
 |-  ( N e. NN -> ( F u. { <. ( ( N - 1 ) + 1 ) , B >. } ) = ( F u. H ) )
14 13 eqeq2d 
 |-  ( N e. NN -> ( G = ( F u. { <. ( ( N - 1 ) + 1 ) , B >. } ) <-> G = ( F u. H ) ) )
15 14 3anbi3d 
 |-  ( N e. NN -> ( ( F : ( 1 ... ( N - 1 ) ) --> A /\ B e. A /\ G = ( F u. { <. ( ( N - 1 ) + 1 ) , B >. } ) ) <-> ( F : ( 1 ... ( N - 1 ) ) --> A /\ B e. A /\ G = ( F u. H ) ) ) )
16 9 oveq2d 
 |-  ( N e. NN -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
17 16 feq2d 
 |-  ( N e. NN -> ( G : ( 1 ... ( ( N - 1 ) + 1 ) ) --> A <-> G : ( 1 ... N ) --> A ) )
18 9 fveqeq2d 
 |-  ( N e. NN -> ( ( G ` ( ( N - 1 ) + 1 ) ) = B <-> ( G ` N ) = B ) )
19 17 18 3anbi12d 
 |-  ( N e. NN -> ( ( 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 e. NN -> ( ( F : ( 1 ... ( N - 1 ) ) --> A /\ B e. A /\ G = ( F u. H ) ) <-> ( G : ( 1 ... N ) --> A /\ ( G ` N ) = B /\ F = ( G |` ( 1 ... ( N - 1 ) ) ) ) ) )