Metamath Proof Explorer

Theorem fseq1p1m1

Description: Add/remove an item to/from the end of a finite sequence. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 7-Mar-2014)

Ref Expression
Hypothesis fseq1p1m1.1 
|- H = { <. ( N + 1 ) , B >. }
Assertion fseq1p1m1 
|- ( N e. NN0 -> ( ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) <-> ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fseq1p1m1.1 
 |-  H = { <. ( N + 1 ) , B >. }
2 simpr1 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> F : ( 1 ... N ) --> A )
3 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
4 3 adantr 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( N + 1 ) e. NN )
5 simpr2 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> B e. A )
6 fsng 
 |-  ( ( ( N + 1 ) e. NN /\ B e. A ) -> ( H : { ( N + 1 ) } --> { B } <-> H = { <. ( N + 1 ) , B >. } ) )
7 1 6 mpbiri 
 |-  ( ( ( N + 1 ) e. NN /\ B e. A ) -> H : { ( N + 1 ) } --> { B } )
8 4 5 7 syl2anc 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> H : { ( N + 1 ) } --> { B } )
9 5 snssd 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> { B } C_ A )
10 8 9 fssd 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> H : { ( N + 1 ) } --> A )
11 fzp1disj 
 |-  ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/)
12 11 a1i 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/) )
13 2 10 12 fun2d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( F u. H ) : ( ( 1 ... N ) u. { ( N + 1 ) } ) --> A )
14 1z 
 |-  1 e. ZZ
15 simpl 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> N e. NN0 )
16 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
17 1m1e0 
 |-  ( 1 - 1 ) = 0
18 17 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
19 16 18 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
20 15 19 eleqtrdi 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
21 fzsuc2 
 |-  ( ( 1 e. ZZ /\ N e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
22 14 20 21 sylancr 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
23 22 eqcomd 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( 1 ... N ) u. { ( N + 1 ) } ) = ( 1 ... ( N + 1 ) ) )
24 23 feq2d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( F u. H ) : ( ( 1 ... N ) u. { ( N + 1 ) } ) --> A <-> ( F u. H ) : ( 1 ... ( N + 1 ) ) --> A ) )
25 13 24 mpbid 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( F u. H ) : ( 1 ... ( N + 1 ) ) --> A )
26 simpr3 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> G = ( F u. H ) )
27 26 feq1d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( G : ( 1 ... ( N + 1 ) ) --> A <-> ( F u. H ) : ( 1 ... ( N + 1 ) ) --> A ) )
28 25 27 mpbird 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> G : ( 1 ... ( N + 1 ) ) --> A )
29 ovex 
 |-  ( N + 1 ) e. _V
30 29 snid 
 |-  ( N + 1 ) e. { ( N + 1 ) }
31 fvres 
 |-  ( ( N + 1 ) e. { ( N + 1 ) } -> ( ( G |` { ( N + 1 ) } ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) ) )
32 30 31 ax-mp 
 |-  ( ( G |` { ( N + 1 ) } ) ` ( N + 1 ) ) = ( G ` ( N + 1 ) )
33 26 reseq1d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( G |` { ( N + 1 ) } ) = ( ( F u. H ) |` { ( N + 1 ) } ) )
34 ffn 
 |-  ( F : ( 1 ... N ) --> A -> F Fn ( 1 ... N ) )
35 fnresdisj 
 |-  ( F Fn ( 1 ... N ) -> ( ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/) <-> ( F |` { ( N + 1 ) } ) = (/) ) )
36 2 34 35 3syl 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( ( 1 ... N ) i^i { ( N + 1 ) } ) = (/) <-> ( F |` { ( N + 1 ) } ) = (/) ) )
37 12 36 mpbid 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( F |` { ( N + 1 ) } ) = (/) )
38 37 uneq1d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( F |` { ( N + 1 ) } ) u. ( H |` { ( N + 1 ) } ) ) = ( (/) u. ( H |` { ( N + 1 ) } ) ) )
39 resundir 
 |-  ( ( F u. H ) |` { ( N + 1 ) } ) = ( ( F |` { ( N + 1 ) } ) u. ( H |` { ( N + 1 ) } ) )
40 uncom 
 |-  ( (/) u. ( H |` { ( N + 1 ) } ) ) = ( ( H |` { ( N + 1 ) } ) u. (/) )
41 un0 
 |-  ( ( H |` { ( N + 1 ) } ) u. (/) ) = ( H |` { ( N + 1 ) } )
42 40 41 eqtr2i 
 |-  ( H |` { ( N + 1 ) } ) = ( (/) u. ( H |` { ( N + 1 ) } ) )
43 38 39 42 3eqtr4g 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( F u. H ) |` { ( N + 1 ) } ) = ( H |` { ( N + 1 ) } ) )
44 ffn 
 |-  ( H : { ( N + 1 ) } --> A -> H Fn { ( N + 1 ) } )
45 fnresdm 
 |-  ( H Fn { ( N + 1 ) } -> ( H |` { ( N + 1 ) } ) = H )
46 10 44 45 3syl 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( H |` { ( N + 1 ) } ) = H )
47 33 43 46 3eqtrd 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( G |` { ( N + 1 ) } ) = H )
48 47 fveq1d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( G |` { ( N + 1 ) } ) ` ( N + 1 ) ) = ( H ` ( N + 1 ) ) )
49 1 fveq1i 
 |-  ( H ` ( N + 1 ) ) = ( { <. ( N + 1 ) , B >. } ` ( N + 1 ) )
50 fvsng 
 |-  ( ( ( N + 1 ) e. NN /\ B e. A ) -> ( { <. ( N + 1 ) , B >. } ` ( N + 1 ) ) = B )
51 49 50 eqtrid 
 |-  ( ( ( N + 1 ) e. NN /\ B e. A ) -> ( H ` ( N + 1 ) ) = B )
52 4 5 51 syl2anc 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( H ` ( N + 1 ) ) = B )
53 48 52 eqtrd 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( G |` { ( N + 1 ) } ) ` ( N + 1 ) ) = B )
54 32 53 eqtr3id 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( G ` ( N + 1 ) ) = B )
55 26 reseq1d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( G |` ( 1 ... N ) ) = ( ( F u. H ) |` ( 1 ... N ) ) )
56 incom 
 |-  ( { ( N + 1 ) } i^i ( 1 ... N ) ) = ( ( 1 ... N ) i^i { ( N + 1 ) } )
57 56 12 eqtrid 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( { ( N + 1 ) } i^i ( 1 ... N ) ) = (/) )
58 ffn 
 |-  ( H : { ( N + 1 ) } --> { B } -> H Fn { ( N + 1 ) } )
59 fnresdisj 
 |-  ( H Fn { ( N + 1 ) } -> ( ( { ( N + 1 ) } i^i ( 1 ... N ) ) = (/) <-> ( H |` ( 1 ... N ) ) = (/) ) )
60 8 58 59 3syl 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( { ( N + 1 ) } i^i ( 1 ... N ) ) = (/) <-> ( H |` ( 1 ... N ) ) = (/) ) )
61 57 60 mpbid 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( H |` ( 1 ... N ) ) = (/) )
62 61 uneq2d 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( F |` ( 1 ... N ) ) u. ( H |` ( 1 ... N ) ) ) = ( ( F |` ( 1 ... N ) ) u. (/) ) )
63 resundir 
 |-  ( ( F u. H ) |` ( 1 ... N ) ) = ( ( F |` ( 1 ... N ) ) u. ( H |` ( 1 ... N ) ) )
64 un0 
 |-  ( ( F |` ( 1 ... N ) ) u. (/) ) = ( F |` ( 1 ... N ) )
65 64 eqcomi 
 |-  ( F |` ( 1 ... N ) ) = ( ( F |` ( 1 ... N ) ) u. (/) )
66 62 63 65 3eqtr4g 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( ( F u. H ) |` ( 1 ... N ) ) = ( F |` ( 1 ... N ) ) )
67 fnresdm 
 |-  ( F Fn ( 1 ... N ) -> ( F |` ( 1 ... N ) ) = F )
68 2 34 67 3syl 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( F |` ( 1 ... N ) ) = F )
69 55 66 68 3eqtrrd 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> F = ( G |` ( 1 ... N ) ) )
70 28 54 69 3jca 
 |-  ( ( N e. NN0 /\ ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) ) -> ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) )
71 simpr1 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> G : ( 1 ... ( N + 1 ) ) --> A )
72 fzssp1 
 |-  ( 1 ... N ) C_ ( 1 ... ( N + 1 ) )
73 fssres 
 |-  ( ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( 1 ... N ) C_ ( 1 ... ( N + 1 ) ) ) -> ( G |` ( 1 ... N ) ) : ( 1 ... N ) --> A )
74 71 72 73 sylancl 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( G |` ( 1 ... N ) ) : ( 1 ... N ) --> A )
75 simpr3 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> F = ( G |` ( 1 ... N ) ) )
76 75 feq1d 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( F : ( 1 ... N ) --> A <-> ( G |` ( 1 ... N ) ) : ( 1 ... N ) --> A ) )
77 74 76 mpbird 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> F : ( 1 ... N ) --> A )
78 simpr2 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( G ` ( N + 1 ) ) = B )
79 3 adantr 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( N + 1 ) e. NN )
80 nnuz 
 |-  NN = ( ZZ>= ` 1 )
81 79 80 eleqtrdi 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
82 eluzfz2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
83 81 82 syl 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
84 71 83 ffvelrnd 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( G ` ( N + 1 ) ) e. A )
85 78 84 eqeltrrd 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> B e. A )
86 ffn 
 |-  ( G : ( 1 ... ( N + 1 ) ) --> A -> G Fn ( 1 ... ( N + 1 ) ) )
87 71 86 syl 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> G Fn ( 1 ... ( N + 1 ) ) )
88 fnressn 
 |-  ( ( G Fn ( 1 ... ( N + 1 ) ) /\ ( N + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( G |` { ( N + 1 ) } ) = { <. ( N + 1 ) , ( G ` ( N + 1 ) ) >. } )
89 87 83 88 syl2anc 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( G |` { ( N + 1 ) } ) = { <. ( N + 1 ) , ( G ` ( N + 1 ) ) >. } )
90 opeq2 
 |-  ( ( G ` ( N + 1 ) ) = B -> <. ( N + 1 ) , ( G ` ( N + 1 ) ) >. = <. ( N + 1 ) , B >. )
91 90 sneqd 
 |-  ( ( G ` ( N + 1 ) ) = B -> { <. ( N + 1 ) , ( G ` ( N + 1 ) ) >. } = { <. ( N + 1 ) , B >. } )
92 78 91 syl 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> { <. ( N + 1 ) , ( G ` ( N + 1 ) ) >. } = { <. ( N + 1 ) , B >. } )
93 89 92 eqtrd 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( G |` { ( N + 1 ) } ) = { <. ( N + 1 ) , B >. } )
94 1 93 eqtr4id 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> H = ( G |` { ( N + 1 ) } ) )
95 75 94 uneq12d 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( F u. H ) = ( ( G |` ( 1 ... N ) ) u. ( G |` { ( N + 1 ) } ) ) )
96 simpl 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> N e. NN0 )
97 96 19 eleqtrdi 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
98 14 97 21 sylancr 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
99 98 reseq2d 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( G |` ( 1 ... ( N + 1 ) ) ) = ( G |` ( ( 1 ... N ) u. { ( N + 1 ) } ) ) )
100 resundi 
 |-  ( G |` ( ( 1 ... N ) u. { ( N + 1 ) } ) ) = ( ( G |` ( 1 ... N ) ) u. ( G |` { ( N + 1 ) } ) )
101 99 100 eqtr2di 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( ( G |` ( 1 ... N ) ) u. ( G |` { ( N + 1 ) } ) ) = ( G |` ( 1 ... ( N + 1 ) ) ) )
102 fnresdm 
 |-  ( G Fn ( 1 ... ( N + 1 ) ) -> ( G |` ( 1 ... ( N + 1 ) ) ) = G )
103 71 86 102 3syl 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( G |` ( 1 ... ( N + 1 ) ) ) = G )
104 95 101 103 3eqtrrd 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> G = ( F u. H ) )
105 77 85 104 3jca 
 |-  ( ( N e. NN0 /\ ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) -> ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) )
106 70 105 impbida 
 |-  ( N e. NN0 -> ( ( F : ( 1 ... N ) --> A /\ B e. A /\ G = ( F u. H ) ) <-> ( G : ( 1 ... ( N + 1 ) ) --> A /\ ( G ` ( N + 1 ) ) = B /\ F = ( G |` ( 1 ... N ) ) ) ) )